4 ms·
ML was written as the language used by the theorem prover LCF. It was written in Lisp.
by lispm 3y ago
ML was written as the language used by the theorem prover LCF. It was written in Lisp.
- JonChesterfield 3y agoI didn't know that link, searches seem to confirm. Thank you. The LCF style provers rely on the host language type system. A theorem instance can only be created by the trusted kernel. Lisp doesn't obviously lend itself to that - you could represent the proof, but I'm not clear how you'd prevent forging one.