[HN Gopher] The Little Prover
       ___________________________________________________________________
        
       The Little Prover
        
       Author : tosh
       Score  : 70 points
       Date   : 2022-09-13 10:02 UTC (1 days ago)
        
 (HTM) web link (the-little-prover.github.io)
 (TXT) w3m dump (the-little-prover.github.io)
        
       | Bilal_io wrote:
       | The MIT Press URL says "Book not found..."
        
         | Jtsummers wrote:
         | https://mitpress.mit.edu/9780262330572/the-little-prover/
        
       | worldsayshi wrote:
       | Are there any suggesters built on top of these proof assistants
       | that have been suggested recently? Like code completion engines
       | but for proofs?
        
         | worldsayshi wrote:
         | Also, has anyone tried building a puzzle game using a proof
         | assistant?
        
       | alecco wrote:
       | There's a nice Corecursive podcast episode with the authors about
       | their last book.
       | 
       | https://corecursive.com/023-little-typer-and-pie-language/
        
       | ketralnis wrote:
       | > Errata
       | 
       | > Pages 165-166: replace all occurrences of "cheese" by "eggs"
       | 
       | Love it
        
         | siddboots wrote:
         | We've all made that mistake before.
        
       | javcasas wrote:
       | This is a very good book that will teach you the basics of
       | manipulating code in a correct way (correct as in mathematically
       | correct, not in some nebulously ill-defined level of
       | correctness).
       | 
       | if-nest-a FTW!
        
         | [deleted]
        
       | smaddox wrote:
       | Another very small proof system:
       | https://github.com/moonad/formcorejs
       | 
       | The core implementation is under 700 lines of JS, including the
       | parser:
       | https://github.com/moonad/FormCoreJS/blob/master/FormCore.js
       | 
       | The author has since moved on to building a runtime with optimal
       | evaluation (https://github.com/kindelia/hvm) and a new proof
       | language on top of that (https://github.com/Kindelia/Kind2) with
       | considerably better performance than existing proof systems.
        
         | voxl wrote:
         | The hype of Blockchain is an astounding thing, and the
         | cascading hype for systems merely because they are based off
         | people in the Blockchain space is equally as befuddling.
         | 
         | Try https://github.com/AndrasKovacs/smalltt if you want a
         | system that considers the things modern systems care about:
         | elaboration and unification.
        
       ___________________________________________________________________
       (page generated 2022-09-14 23:00 UTC)