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

[graydon]

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

Comments

Re: POPLmark challenge

[ext_1472537]

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 substitution in a non-erroneous way in order to make progress on this sort of problem using Coq. As I mentioned we went on to use Twelf to solve this sort of problem at scale without any significant difficulties. Comparable results have not, to my knowledge, been achieved using any other system.