||[Oct. 27th, 2003|05:29 pm]
So I am "virtually attending" this workshop thing going on between SRI, NASA langley, and here. I am a little depressed how little I understand of any of the talks. Part of the blame goes to the shoddy audio quality. It is very hard to hear what anyone is saying over the teleconferencing equipment.|
Nonetheless Ricky Butler from Langley made some points about the difficulty of managing a large library of formal proofs that really resonated with me, specifically claiming that he thought good naming conventions for lemmas was of paramount importance. Now anyone that's managed to get me to talk about it knows that I have this tendency to rant that it's just fundamentally broken to do programming (and by extention, hacking up formal proofs) via text files that only know how to connect a reference to a function, say (or a lemma) to the definition of that function (or the proof of that lemma) via a single, fixed string of glyphs that the programmer has to agree on early, and type in every time she wants to use its referent.
I think I would be much happier living in an environment where I just create things which are functions or are lemmas, and live in some nice organized hierarchy incidentally, and have names incidentally. However, I might be totally misguided, and I might be massively overestimating the actual practical benefit of my blue-sky dreaming in this direction... when pressed to actually argue why structural editors in general are any good, I always seem to mumble and sputter.