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:
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.
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.
Didn't get to the Monads.
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.