Jason and I have been writing a lot of code for Automated Theorem Proving recently, and enjoying it quite a lot.
I would describe the process of writing this particular piece of code today as "programming by accumulation of invariants."
The whole process of writing this prover is somewhat like the architecting by accumulation of modules. Integrating them into a working thing will, I hope, be easier than the reputation this methodology has due to our foresight and programming language. Yay types!
This is going to be a busy weekend and coming week. I guess it is crunch time after all. The revisions for the LICS paper are due on Sunday, which is really obnoxious because it means I will spend the weekend doing them. I don't really understand 10 page limits on conference papers--suggested lengths are fine, but doesn't it make more sense to simply have peer review determine the appropriate level, content, and length for a submission?
Various things that happened
(17 Apr 2004 at 20:56)
Yesterday I ran the "random distance run." I had free registration because I designed the shirt (front, back), so at the last minute I decided I might as well run. I was not prepared to run 2 miles on a hot day with heavy shorts and change in my pockets, but remember: 49th out of 50 is the last winner.
I saw Kill Bill #2. I liked it better than the first one, actually. It is recommended if you like Tarantino and kung fu.
A real use for polymorphic recursion: stable mergesort. In the split phase, tag each element with its index. Then the comparison function becomes lexicographic(old_compare, int_compare). By hoisting the indices out into a pre-pass, you can avoid having to recurse on a different list type each time, and despite this code being more efficient, it is somehow not as nice. (Think of a proof of its correctness--you get stability relative to the original list, not the passed in lists, inductively.)
Several of my friends from undergrad are here visiting, as is standard for carnival. We hung out some yesterday. In typical form I am spending the nice day working on projects. I got sidetracked from working on new escape server stuff, an unimplemented bit of Aphaisa 2 left me unable to write a program in the way I wanted to. So today I finally implemented constant patterns in Aphasia 2's massively complicated pattern compiler. This is not my first pattern compiler, but there are still things I'd do differently if I were to rewrite it from scratch. If only I could remember what they are...?
Five elements of thought set
(13 Apr 2004 at 23:40)
Today I got four consecutive free games (two earned, two "match") in Medieval Madness at the O.
Pollard's "Flat Beauty" is in my top five favorite songs ever recorded ever, definitely.
If there is an addiction for writing optimization passes for fun in my spare time, then I have that.
I wish I could send all the candy in my house back in time to when I was young and wouldn't mind the stomach ache it causes me.
I also wish I could show my eight-year-old self the fucken explosions in "Legend of Zelda: The Wind Waker," which are also in my top five favorite computer rendered explosions ever rendered ever, definitely.
Today had beautiful weather in Pittsburgh, so we went on a trip to Schenley park today to try out my new(ish) macro lens in the wild. I took a load of photos; my favorites are now in my photo gallery in the New! section.
I just saw this Wired Article talking about a site (webjay) that collects playlists of music that can be found for free on the web. My own song "Testify in Hockey" heads up the playlist dedicated to Condoleezza Rice called "testify." (That one is weird enough to be listed in the Wired article!) Speaking of Condi, she came across as extremely evasive in her testimony, as far as I'm concerned.
By the way, I think that services like Webjay (except much more sophisticated) are the future of music--not buying and selling digitally or physically.
Well, after finishing up my paper last week and recovering over the course of the weekend, I can finally get back to what I really love: Pikmin, Zelda: the Wind Waker, hacking on projects (I made a significant modification to aphasia last week that should cut down on or eliminate the occasional timeouts (which manifest as crash messages), and I have several additions in the works for escape), automated theorem proving, and formalizing proofs in machine-checkable Twelf format.
Thus completes my semesterly all-nighter. 5:00am is not a very good time for a deadline, especially if your ISP goes down from 4:53am-4:57am. But I got the paper in, and even gave it a proofreading pass. You can read it if you like: Functional Grid Programming with ConCert. It should be somewhat more readable than the last one, but also somehow less academic, and so, I can't help but feel less proud of it. We'll see how ICFP likes it.
Right now I am "in the zone" finishing up my ICFP 2004 submission on my old compiler. It's due at like 11:00pm Samoan time, which is 5:00am in Pittsburgh. Well, I'm not really in the zone because I'm writing this entry (by way of pysching myself up for writing stuff like the related work and introductory paragraph, which are typically my least favorite sections to write), but pretty soon I will be back in that zone, finishing up the painful sections and proofreading and making pretty diagrams in Illustrator. I have even got some really chill shit on; stuff that I hardly ever have the patience for anymore like Labradford and GSYBE!. Okay, enough chilling. I'll see you at 5:00am.