NAMIN-XO

Since learning about the Curry-Howard isomorphism, I’ve been looking more closely at type theory, starting with the freely available and well-written book, Type Theory and Functional Programming. But now, I’ve been wanting to play with some type systems more. I looked at LambdaPi, which prompted me to review my basics. So I jumped to Pierce’s class, Software Foundations, which he discusses in Lambda The Ultimate TA. The lectures/scripts are a great and simple way to learn Coq. I’ve only just finished lecture 3, and I finally understand Coq’s role as a proof assistant. I am planning to work through the entire set of lectures.

I completed all the projects I wanted to from The Elements of Computing Systems (my Amazon review). I did 10 out of 12 projects, just leaving out projects 9 and 12 (the ones involving high-level programming in Jack). I had a lot of fun. My favorite project was project 8, which completed the VM translator. I learned a lot all the way (though, perhaps, less than I thought I would in the last project, the compiler from Jack to the VM). Highly recommended.
I am not sure whether TECS will be enough to prepare me for my Computer Architecture class. I definitely have the big picture of architecture in mind now, but I might need to supplement it with some 6.004 readings.

I went to the library today to check out Munkres’ Topology, because I am interested in listening in 18.901 next fall. I couldn’t find it except on Reserve, so I checked out some lighter readings:

• A Topological Aperitif
• The Hitchhiker’s Guide to Calculus by Michael Spivak (my Amazon review)
• Calculus on Manifolds by Michael Spivak

I got the Spivak’s books because Gerry Sussman recommends Calculus on Manifolds in Structure and Interpretation of Classical Mechanics (SICM), where he mentions that his notation is inspired from Spivak’s.

This term was a lot of fun. Specially Sussman’s class. In fact, I liked it so much that I am thinking of taking his other class next term (the idea of expressing a physical theory as an unambiguous computer program really appeals to me). Then, for my second class, which has to be in Systems (and unfortunately, there isn’t that many options next fall!), I hesitate between Operating Systems and Computer Architecture. I feel Computer Architecture might be more useful in the long run, specially for someone like me who hasn’t taken a solid undergrad class in architecture. However, I heard it’s boring, and Operating Systems is sure to be more fun (though probably more time-consuming!), as I’d get to write my own operating systems from scratch in the labs.

On to achievements:

• In Sussman’s class, my team and I had a really great time on the final project. We used the great book Building Problem Solvers (my Amazon review) as a base to implement a debugger for metabolic networks, BioHacker.
• In my research, I finally released my work as a real product, Micado. The latest feature I’ve added is automatic control inference & generation, though this is still not officially included yet.

Now, I only have my film music exam on Wednesday. I don’t think I’ll study much for it. Instead, I’ll be reading a few books:

• Reasoning about Uncertainty (my Amazon review) (at books24×7)
• The Elements of Computing Systems (my Amazon review) — This will be my primer substitute for 6.004. I intend to work through all the projects during the course of the summer.

I posted a review of Expert F# on Amazon.

I really enjoyed the book, the Reasoned Schemer. I would also suggest the papers from Will Byrd as follow-ups to the book. Here is some bits of code I’ve written using the book’s system.

After browsing the Little Schemer, I got inspired to write a derivation of the Y combinator.

I am reading the book Visualizing Data by the creator of the Processing. So far, so good.