[HN Gopher] VLISP: A Verified Implementation of Scheme (1993) [pdf]
       ___________________________________________________________________
        
       VLISP: A Verified Implementation of Scheme (1993) [pdf]
        
       Author : servytor
       Score  : 44 points
       Date   : 2021-12-29 19:17 UTC (3 hours ago)
        
 (HTM) web link (mirror.informatimago.com)
 (TXT) w3m dump (mirror.informatimago.com)
        
       | ghettoimp wrote:
       | 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/
        
       | liups wrote:
       | Cool work.
       | 
       | I wonder if contemporary proof assistants have enough primitives
       | to implement this.
        
       | servytor wrote:
       | People may also be interested in BitC[0] in regards to verified
       | lisp languages.
       | 
       | [0]: http://yamm.finance/wiki/BitC.html (the best summary I could
       | find)
        
       ___________________________________________________________________
       (page generated 2021-12-29 23:00 UTC)