Tried doing some of the category theory model solutions. Wrote up a clean solution of the infamous assignment 5, problem 2, but got sidetracked by digesting a neat paper Kevin Milans mentioned to me as we were chatting at one point: Generating the Greatest Common Divisor, and Limitations of Primitive Recursive Algorithms . The first proposition in the paper asserts the unboundedness of the "distance" from {a,b} to gcd(a,b) in terms of the number of addition, subtraction, division or mod operations you use, and it whips out fairly beefy model theoretic concepts (an aleph-1 saturated elementary extension of the integers as an ordered ring) already in the first line. I think I believe the proof now, but I'm still working on seeing if I can get it pared down to an elementary argument. Also went to Alex Nanevsky's thesis proposal. Neat stuff. I should also bug trurl about his thoughts and work on modal types and partial evaluation some time.