constructive logic
today, I am working on the eighth constructive logic assignment and also studying for the second midterm for same. I am told that last year, at around this point in the semester, they moved on to talk about various other logics. this semester, we have been doing prolog and twelf, and it has had me on edge. up through the proof checker assignment, I found everything engaging and interesting, but now it has seemed like the class has transitioned from "teach about this logic system" to "look what i can do with this obscure language, let's have the students do this too".
it is probably worth noting at this point that when I entered lecture yesterday a good amount late, I saw frank twelfing it up just as in the previous several lectures, and my thoughts immediately began wandering to other actually thought-provoking logic foo: I proceeded to spend the entire lecture talking about infinite logics on #cslounge with mrwright, which I found much more fulfilling than the prospect of spending all my attention on watching twelf code be written.
several assignments ago, we wrote a proof checker in SML (it was said by veterans that a different language would have been better, but I was okay with that since I am comfortable with SML). you would feed it a proposition, and it would apply rules and say "yes, this is provable", or "no". it was quite cool. now, the current assignment is certified theorem proving, which means in addition to "yes" or "no", the proof checker should also tell what the proof is. for doing this, they have ported the proof checker over to twelf, which apparently naturally wants to spit out the proof as it goes along. in my experience so far, twelf is very clever conceptually but a sizable pain to actually work with. now, the systems-oriented hacker in me says "just hack up the SML checker to generate a proof", which would be unpleasant stylistically but overall very doable. this assignment, on the other hand, is seeming like nothing but jumping through a lot of hoops, figuring out the obscure syntax, and doing nothing actually requiring of thought that I haven't done before.
in short, I would like for the culminating parts of this course to feel more like a polishing up of the thought-provoking subjects we were taught during the first half, and less like a program of indoctrinating the undergrads with an introduction to the sort of stuff that the graduate researchers do - not that I have anything against that sort of research, but I cannot bring myself to personally care about it, and thus doing this sort of assignment feels very inappropriate.
it is probably worth noting at this point that when I entered lecture yesterday a good amount late, I saw frank twelfing it up just as in the previous several lectures, and my thoughts immediately began wandering to other actually thought-provoking logic foo: I proceeded to spend the entire lecture talking about infinite logics on #cslounge with mrwright, which I found much more fulfilling than the prospect of spending all my attention on watching twelf code be written.
several assignments ago, we wrote a proof checker in SML (it was said by veterans that a different language would have been better, but I was okay with that since I am comfortable with SML). you would feed it a proposition, and it would apply rules and say "yes, this is provable", or "no". it was quite cool. now, the current assignment is certified theorem proving, which means in addition to "yes" or "no", the proof checker should also tell what the proof is. for doing this, they have ported the proof checker over to twelf, which apparently naturally wants to spit out the proof as it goes along. in my experience so far, twelf is very clever conceptually but a sizable pain to actually work with. now, the systems-oriented hacker in me says "just hack up the SML checker to generate a proof", which would be unpleasant stylistically but overall very doable. this assignment, on the other hand, is seeming like nothing but jumping through a lot of hoops, figuring out the obscure syntax, and doing nothing actually requiring of thought that I haven't done before.
in short, I would like for the culminating parts of this course to feel more like a polishing up of the thought-provoking subjects we were taught during the first half, and less like a program of indoctrinating the undergrads with an introduction to the sort of stuff that the graduate researchers do - not that I have anything against that sort of research, but I cannot bring myself to personally care about it, and thus doing this sort of assignment feels very inappropriate.