(no title)

Notes from a Medium-Sized Island

Jason

[	website	\|	My Website	]
[	userinfo	\|	livejournal userinfo	]
[	archive	\|	journal archive	]

	[Oct. 27th, 2003\|05:29 pm] Jason
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.
Link	Reply

Comments:

From:

kaustuv
2003-10-27 05:33 pm (UTC)

I'd agree with you on bound variables; they are not informative, so they should not be named. Reusable functions, on the other hand, are informative objects, and we all know that information wants to be free.

Now, you could argue that my free variable is your bound variable, and we'd be back to square one. That's why I'll just say that so what if big lambdas have little lambdas in them, and little lambdas have littler ones still? At some point we just have to decide that some lambdas are just too precious, and unchain them.

So I don't buy your Wallian "fundamentally broken" rant. ("It's fundamentally broken to have only fifteen different ways to bake your goose! Perl has over seventy ways to do it, including a one-liner using the Perl regular expression library to define a general 'warm feathered biped' functionality.")

(Yes, they call me the Sir Mix-a-lot of metaphors.)

(Reply) (Thread)

From:

jcreed
2003-10-27 08:29 pm (UTC)

I'm not saying that functions shouldn't have names. But the way in which they have just one name seems wrong to me somehow. On the other hand, now that I say that, it sounds stupid to complain about things having unique names.

(Reply) (Parent) (Thread)

From:

ssaiscps
2003-10-28 07:46 am (UTC)

Lemma A = Foo.
Lemma B = Foo.
...

(Reply) (Parent) (Thread)