|
|
|
|
|
|
by ghettoimp
1638 days ago
|
|
|
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. [1] https://www.cl.cam.ac.uk/~mom22/jitawa/
[2] https://cakeml.org/ |
|
|