FWIW -- 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.
3 comments
[ 3.4 ms ] story [ 28.2 ms ] threadI wonder if contemporary proof assistants have enough primitives to implement this.
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/ [2] https://cakeml.org/
[0]: http://yamm.finance/wiki/BitC.html (the best summary I could find)