Skip to content

eneoli/alice

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

🔍 Alice - A Constructive Logic Proof Checker

GitHub Workflow Commit Activity Last Commit Top Language Repo Size

About

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

Build Instructions

Prerequisites

To build Alice, ensure that you have the following installed:

  1. Rust: Install Rust from rust-lang.org.
  2. wasm-pack: Install wasm-pack from rustwasm.github.io.
  3. NodeJs and NPM: Install NodeJs and NPM from nodejs.org.

Step 1: Build the WebAssembly Binary of the Backend

In the root directory of the project, run the following command to build the WebAssembly binary:

wasm-pack build

Step 2: Build the Frontend

Navigate to the frontend directory. Make sure the required dependencies are installed by running npm install. Then run

npm run build

This will bundle the frontend assets and the WebAssembly binary and the final files will be output to the dist folder in the project root directory. These can be served by any HTTP server.

Tests

Alice has a series of autmatic tests. To run them, make sure you are in the project root directory and run:

cargo test

License

Alice is licensed under the MIT License. See LICENSE for the full license text.