Alice is a tool for verifying proofs in constructive logic, specifically designed to assist students in the study of constructive logic.
Constructive logic, also known as intuitionistic logic, is a form of logic that emphasizes the constructive nature of proofs. Alice provides an interactive user interface in the notion of natural deduction, where students can learn by doing — constructing proofs step by step, with immediate feedback and support.
In addition to the graphical user interface, Alice includes its own mini programming language that emphasizes the beauty of the Curry-Howard Isomorphism. This isomorphism links logic and computation and is the foundation of modern proof assistants like Lean and Coq. It can be experienced within Alice by seamlessly switching between the graphical user interface and a code editor while constructing proofs, helping to bridge the gap between theory and practical application in proof assistants.
Alice is served as a standalone web app, using Rust and WebAssembly for its backend and React for the frontend.
alice-showcase.mp4
Alice is licensed under the MIT License. See LICENSE for the full license text.