4 ms·
VLISP: A Verified Implementation of Scheme (1993) [pdf]
- liups 5y agoCool work. I wonder if contemporary proof assistants have enough primitives to implement this.
- ghettoimp 5y agoFWIW -- A later, vaguely related project was Jitawa[1]. Its Lisp dialect was not as fancy as VLISPs, but its verification was much more thorough (machine checked proofs down to the X86 code for the runtime.) Today, ongoing, CakeML[2] extends these techniques to an ML language and is just generally super awesome. [1] https://www.cl.cam.ac.uk/~mom22/jitawa/ https://www.cl.cam.ac.uk/~mom22/jitawa/ [2] https://cakeml.org/ https://cakeml.org/
- servytor 5y agoPeople may also be interested in BitC[0] in regards to verified lisp languages. [0]: http://yamm.finance/wiki/BitC.html http://yamm.finance/wiki/BitC.html (the best summary I could find)