Comments | graydon: technicalities: specs (Lisp, ML, ALGOL, Ada, JS2, ES4, RnRS, Redex, POPLmark, Rust, K, Comp/JSCert)

graydon

technicalities: specs (Lisp, ML, ALGOL, Ada, JS2, ES4, RnRS, Redex, POPLmark, Rust, K, Comp/JSCert)

Feb 06, 2014 09:17

According to the History of Programming Languages website (currently offline) there have been somewhere around 8500 programming languages developed since the Autocodes of the early 50s. The internet archive has scraped HOPL's taxonomy at least as well as a few references and at least the primary year indexes (the year of my birth, for exampleIt's ( Read more... )

tech

Comments 6

mechanization of standard ml ext_1472537 February 7 2014, 04:18:17 UTC

Karl Crary and I completed a mechanization of the semantics of Standard ML more than five years ago. It's about 30,000 lines of Twelf code, which we wrote by pair-programming together over the course of a semester, meeting one day per week for about two hours or so each time. A big part of this work was reported in our POPL paper with Daniel K Lee, and we subsequently published the tar ball of the entire proof of type safety for the full language. It was the first such mechanization effort at scale, to my knowledge, and has not been matched since by any widely-used language.

Re: mechanization of standard ml graydon February 7 2014, 21:13:29 UTC

Cool! That's an impressive bit of work, congratulations! I think I did not see it when it was published.

POPLmark challenge ext_1472537 February 7 2014, 04:20:12 UTC

I would also mention that Karl Crary, Michael Ashley-Rollman, and I "won" the POPLmark challenge (it was, after all, a competition) by providing a complete solution within two weeks of the announcement of the challenge. The first partial solution in Coq only arrived 6 months later; I am not sure whether any full solution was achieved subsequently.

Re: POPLmark challenge ext_1472537 February 7 2014, 17:45:04 UTC

I should have said, but maybe it goes without saying, that we used Twelf, and built on the Harper-Stone methodology for defining Standard ML.

Incidentally, the stated purpose of the POPLmark challenge was to determine which system was best for doing mechanized metatheory. Obviously Twelf won hands-down, but it seems that that was not the intended answer, and the result was accepted grudgingly and was subsequently ignored.

Re: POPLmark challenge graydon February 7 2014, 21:08:30 UTC

I don't quite know how to respond to this in a way that's not offensive; I want to assure you that I have no horse in this race and it's entirely possible that Twelf Is Better Than Coq (which seems to be what you're getting at). I apologize for giving short shrift to Twelf. I don't actually know how to evaluate them; I don't think POPLmark can tell us that.

For what it's worth: I never got the impression that the challenge was a "pick-a-winner" competition of systems. If you look at the initial posting it seems clear to me that the organizers just wanted to get a very general "sense of the field", stimulate discussion, see some approaches people would take on benchmark problems (which are still "toy sized" relative to industrial PL problems, but whatever).

As a (now-ex) paid PL designer (not a logical-framework expert, much less the author/designer of one) I still don't know how how to evaluate the POPLmark results. I don't understand the submissions especially well, I can't give a particularly compelling description of the ( ... )

Re: POPLmark challenge ext_1472537 February 8 2014, 05:12:29 UTC

In my opinion it does not make sense to say that disparate systems such as Twelf and Coq are better than one another. So I am not saying that. What I am saying is that a benchmark was formulated, a challenge was laid, and we won that challenge hands-down using Twelf. If the challenge had been for something other than mechanization of programming language metatheory, then we wouldn't even have entered, because Twelf would not have been suitable to the task. This is perfectly clear, and not in contention. But the idea at the time was to see which system was better for doing language metatheory, and this was the benchmark that was established to test that premise. We didn't choose the benchmark; in fact, it is quite clear from the formulation that the benchmark was chosen to defeat us. Although we showed that Twelf was superior for the given purpose, the proposers just carried on promoting Coq for mechanized metatheory. In fact it is such a poor choice that the currently recommended practice is to use an erroneous notion of ( ... )