3 ms·
Originally ML was implemented in Lisp. It was the language for a theorem prover: HOL https://en.wikipedia.org/wiki/HOL_(proof_assistant) https://en.wikipedia.o
by lispm 11y ago
Originally ML was implemented in Lisp. It was the language for a theorem prover: HOL
https://en.wikipedia.org/wiki/HOL_(proof_assistant) https://en.wikipedia.org/wiki/HOL_(proof_assistant)
Older ML (not something like SML) in Lisp is still available in some old version of that prover.
- nickpsecurity 11y agoInteresting. So, basically taking it full-circle back where it came from. That is, if one still uses it with HOL4 for verification.