Introduction

lsts is a proof assistant and sometimes a programming language. LSTS is designed for assisted reasoning in mathematical proofs. For those feeling particularly adventurous, it may even be possible to use as a programming language.

  • Lightweight. LSTS is only 3K sloc of Rust code with no dependencies.
  • Fast. Benchmarks compare to Rust itself for compilation speed and efficiency.
  • Familiar. The Syntax is usually similar to Coq, ML, or Haskell.

Intended Audience

This tutorial and reference has been compiled for people who have significant mathematical or programming experience and are looking to try something new. LSTS is anything but average. There are still huge pieces of functionality missing from LSTS. There are also huge pieces of functionality that are already outperforming comparable software products. Hopefully this guide will help you find something inspiring. Soon this guide will help you also find something useful. You can help us improve more quickly by suggesting improvements or asking questions.

Contributing

LSTS is free and open source. You can find the source code on GitHub and issues and feature requests can be posted on the GitHub issue tracker. LSTS relies on the community to fix bugs and add features: if you would like to contribute, please read the Code of Conduct guide and consider opening a pull request.

License

The LSTS source and documentation are released under the MIT License.

Copyright Andrew Johnson, 2023.