Wednesday I met my goal of meeting up with people much more! This feels empowering, because it is starting to sink in that I can make choices and then follow through, and that I can have what I want. However, it definitely impacted flow. As it turned out, I did my loner activities before and after hours (blogging and my project), because most of the time during the day I was doing things with other people. That feels like a good way to do it. The other thing was that my nap signal came and went during a tutorial, and when I got around to trying, I slept little. So then I got frazzled in the late afternoon, and I actually went out twice, nominally for food and coffee, but really just to shake off the tiredness.

I hadn't thought about this explicitly until yesterday, but I have a general plan of having a group of projects, one of which is the current priority while the others are gestating. Every day I work on the current project for at least some time, and then optionally I also dabble in other things. When I have satisfied myself with the state of the current project — that is, when the cost of refining it exceeds the value I get from it, I will choose another one to focus one. It is important to me to have something that I am making tangible, if slow progress on. At the same time, I need to explore. So this seems to be working so far.

Here was my plan:

Plan

Actual

Working with others

  • Paired a bit with another person going through the Factor tutorial.

  • Joined the Project Euler group. We all decided to learn Haskell thereby. The second question requires writing Fibonnaci, and so I had to re-relearn tail recursion. I think that's in the first chapter of SICP. That reminds me that I was considering going though SICP and solving the problems in Haskell. Or Factor. Heh.

  • Alan gave a tutorial on Coq. Here are my notes:

    • all proofs are on construction by induction: intuitionist, no law of excluded middle!

    • things that don't prove don't compile

    • not turing complete?!

    • Curry Howard correspondence makes a analogy:

      types <--> propositions

      terms <--> proofs

      • To prove: construct a term/value whose type is the proposition
      • expressions evaluate to types or propositions
      • If the compiler says that the term type-checks to the proposition, then the term is a proof of that proposition.
      • Presumably, if the implementation of an algorithm in eg. Haskell, is isomorphic to a proof in Coq, then this is a proof of correctness of the implementation.
      • tactics is a tool that helps writing proofs.

      Although Alan talked about how Coq is a gentle way for programmers to learn math, it also seemed like a great way for a mathematician to understand the power of type systems. I was really blown away.

Reading

Didn't get to the Monads.

Misc

Reflections

It is tempting to constantly compare myself to others, especially when I see how much they have achieved. I am working hard to resist this. Back in January, some friends and I made New Year's resolutions. I hadn't done that in a very long time, and I finally settled on:

Focus on creating, not achieving.

So I'm practising that.