Jason (jcreed) wrote,

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.

  • (no subject)

    Played some board games at the fb office with newly-arrived-to-nyc dan blandford and some friends-of-friends of his. Codenames and…

  • (no subject)

    This morning I suddenly had a memory of a game I used to play in the mid-late 90s over email. In it you "designed" animals by giving them, like, 4…

  • (no subject)

    Played some more Shenzhen I/O. The later puzzles are getting straight up hard. Had some fun optimizing the earlier ones, though.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded