PeanoScript: TypeScript but it's a theorem prover

PeanoScript is a theorem prover language based on:

  1. A TypeScript-like syntax
  2. First-order logic
  3. Peano axioms

Because many programmers are at least somewhat familiar with these systems (even if they don't know it 🙂), PeanoScript is a great introduction to automated theorem proving.

To make this introduction even smoother, it runs fully on the web, including an interpreter and an advanced language server.

PeanoScript has good support for running proofs as programs, thanks to the Curry-Howard correspondence. Here is an example of a proof that every natural number is either even or odd, which is also a function that returns the parity of a number:

To learn PeanoScript, see the interactive tutorial. There is also reference with a condensed description of the language, and a playground where you can try writing and running code.