p
e
r
s
o
n
a
l |
Not guilty!
(15 Dec 2003 at 20:42) |
I had my first ever date in "traffic court" today for a ticket I recieved for parking in my driveway. In Shadyside, Pittsburgh, even tiny alleyways and driveways have street signs and, sometimes, ridiculous parking regulations. The magistrate was tough but in the end, I was not guilty!
Tomorrow is Black Friday, the School of Computer Science's semesterly herd-thinning ritual. I will probably spend much of the day in the lounge at the all-day "TG" (short for TGIF) party, but I will also take the reprieve to get some work done on my projects, which have been neglected since October so that I could finish Nanowrimo.
Speaking of which: I have decided that writing is fun, but it is not as good as many other projects. The problem is that, after finishing my book, well, there's a certain "doneness" to it that is anticlimactic and tiresome. Contrast to an album-a-day: When I finish one, I want to listen to it, and I can listen to it for several weeks before getting bored. I like my novel, and I am glad that anyone can download it, but I am sick of reading it. Contrast to my current programming project, Escape: When I finish it, there will be still loads of stuff to do. Create levels, play levels that others have created, stare at web logs and wait for you to download it. Speaking of Escape, I got a bit done on it this weekend. I encourage you to download the alpha version linked above and then use the in-game upgrade and level-update to synchronise yourself with the newest version. There are new tiles, and you can now upload your completed levels to my server with a single keypress.
Research is going well. I have a translation between my slightly weird (but nice, I think) type system and a fairly standard system adapted from Simpson; this means that if I prove admissibility of cut for the standard system (which should be easy) then I get it as a consequence for my type system. That's good, because I've been yearning for the whole semester for a logic that supports cut elimination and has a reasonable computational interpretation. Right now I am in the fairly relaxing phase of proving things I expect to be true, which is much better than the agonizing and frustrating phase of trying to prove things that are true but I don't know why, or trying to prove things that are false. (My intuitionist friends: Of course when I refer to objective "classical" truth--in the sense that truth and provability are not identified, or, when feeling especially cynical, truth and provedness--I am speaking informally.)
|  |
|
| Not guilty by reason of parking in your own driveway, or by cop not showing up at court, or what? |
| With respect to name field: Have you considered cookies? Or placing it above the textarea? |
Why above? Because you forget?
I am planning on adding cookies, yeah. Actually, I will do that right now. OK, done. |
| At this traffic court it would be pretty hard for the cop to know when to show up: there are no appointments, you just show up and explain your case in 30 seconds in front of a grumpy magistrate, and she finds you guilty or not guilty. In my case, it was the fact that I was clearly not parked on the street that did it for her. |
| If it makes you feel any better, I've been struggling with some cut-elimination woes for most of the semester myself, although I can't even get to the point where I've settled on an acceptable sequent calculus yet. This is in part because it's hard, in part because my advisor has been out of town for the whole semester, and in part because I'm a lazy fuck. |
|
|
|
|