ProofLang

• 

  ProofLang title.

• 

  ProofLang after receiving several queries for objects and types.

Inspiration

We want to share the beauty of the Curry-Howard isomorphism and automated proof checking with beginning programmers. The concepts of Types and Formal Proofs are central to many aspects of computer science. ProofLang is to Agda the way Python is to C. We believe that the beauty of mathematical proofs and formal verification can be appreciated by more than CS theorists, when taught the right way. The best way to build this intuition is using visualizations, which is what this project aims to do. By presenting types as containers of variants, it allows a teacher to demonstrate the concept of type inhabitation, and why that is central to automated theorem proving.

What it does

ProofLang is a simplified, type-based, programming language. It also comes with an online interpreter and a real time visualization tool, which displays all the types in a way that solidifies the correct type of intuition about types (with regards to theorem proving and the calculus of constructions), alongside the instantiations of the types, showing a ledger of evidence.

How we built it

We wrote ProofLang the programming language itself from the ground up based on the calculus of constructions, but simplified it enough for beginner audiences. The interpreter is written in Rust and complied down to WebAssembly which is imported as a Javascript library into our React frontend.

Challenges we ran into

We ran into challenges integrating WebAssembly with our React frontend. web-pack compiles our Rust code down into Javascript for Node.js rather than the Web JS that React uses. Since the interpreter is written in Rust, there was some fighting with the borrow-checker involved as well.

Accomplishments that we're proud of

We are proud of building our own interpreter! We also created a whole programming language which is pretty awesome. We even wrote a tiny parser combinator framework similar to nom, since we could not figure out a few edge cases.

What's next for ProofLang

Support for function types, as well as type constructors that are not unit-like! Going forward, we would also like to add a visual programming aspect to it, where users can click and drag on a visual interface much like Snap to write code, which would make it even more accessible to beginner programmers and mathematicians.

Built With

• css
• javascript
• react
• rust
• webassembly