(23 Apr 2004 at 21:10)
|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?
|Hi Tom. You should speak ENGLISH sometime. I'm going to a conference too, but it's a conference about babies and baby-based research. I work on a project yelling at babies' mothers in front of them. I'm great.
How are you? I like the idea of writing a personal note in a public forum. I'm interested in general about the seemingly arbitrary boundaries between the public and the private. That's why when I am singing in my car and I'm at a stoplight, I like to croon to the people on either side of me. Other people's discomfort is funny. You should write me sometime, but not here because I probably won't come back to read it.
Well, where do I write you?
|Google is your friend!|
|look at me -- i came back anyway like a jackass. my e-mail address is my last name minus the last letter (at) the school i attend (dot) edu.
|Right, now I remember -- you turned Polish!|