Proofs

LSTS is a theorem prover. LSTS may also be a programming language.

LSTS proofs are built on something called the Curry-Howard Equivalence. The equivalence states and demonstrates that programs are proofs and that proofs are programs. There is a virtuous one-to-one correspondence between proofs and programs. Despite this wonderful finding, most programs do not intend to be proofs. Likewise, most proofs do not intend to be programs.

LSTS is built for this Equivalence. Programs that look like just code, may actually be intended as a proof. Following are some examples of how we can make use of LSTS and the Curry-Howard Equivalence to write better programs and more easily certify proofs.

Copyright Andrew Johnson, 2023.