Cogito

Cogito is a small, simple, and expressive programming language that uses the ACL2 theorem prover to execute functions and prove theorems. Try it out!

• Easy to Learn, Powerful to Use: Familiar syntax and concepts for beginners, while offering advanced features like theorems and functional programming for experienced developers.
• Prove Your Code Works: Go beyond testing by formally proving the correctness of your functions, ensuring your programs behave exactly as intended.
• Built-in Formal Methods: Leverage the power of ACL2, a renowned tool for rigorous software verification, without needing to learn its complex syntax.
• Concise and Readable: Write clear, expressive code using intuitive structures like struct for data and types for safety.
• Functional Programming Made Accessible: Explore a different style of programming based on functions and recursion, unlocking new problem-solving approaches.
• Bridge to Advanced Concepts: A stepping stone to understanding formal verification, functional programming, and the ACL2 ecosystem.

Read more about Cogito's advanced features here.

• Counterexample generation
• More robust structs
• Pattern matching
• Reverse transpilation for error messages

• File issues and send PRs on Github
• Style guide (coming soon!)
• Some thoughts for ACL2 power users

• Rex Page, my Master's thesis advisor and the professor who introduced me to ACL2
• Crafting Interpreters by Robert Nystrom, the basis of my parser and the inspiration for finally tackling this project after over a decade of rumination