3 ms·
Theorem Prover Museum: The Original Edinburgh LCF
- nxobject 2y agoI found this while looking for the first ML-family language (1977!) – a very, very sweet spot in the whole space of programming languages. The first programs written in an ML are tactics/frontend for the theorem prover LCF... it was serendipitous that it turned out to be a good kernel of a language, too. I suspect it is written in whatever Lisp the Stanford AI Lab had kicking around the time: their homespun extension of LISP 1.5. Unfortunately, significant parts are written in LAP ("LISP Assembly"), which seems to assemble into PDP-6/10 machine code.