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:
- Current project Tahoe-LAFS symlinks patch:
- Go through the test_cli.test_ignore_symlinks test line by line and understand it fully.
- integrate Zooko's coverage tool patch, if my time coincides with Zooko's.
- Working with others:
- Meet with the Project Euler folks
- Meet with the Coq folks
- Light reading: Monads for the Curious Programmer, Part 2
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.
Didn't get to the Monads.
- Two of the people I chatted with today have already written a Lisp interpreter. I asked them each how they got started with that. One of them recommended Write Yourself a Scheme in 48 Hours, and the other (How to Write a (Lisp) Interpreter (in Python)). With the latter, I also talked about how surprising it was that it could be done so quickly. He said: "You just have to start." Words to live by.
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.