Finch

Finch is a browser-based editor for writing and checking Fitch-style natural deduction proofs. It supports both propositional logic and first-order logic (various modal logics might be supported later on), and verifies every line of the proof as you type. The application is compiled from Haskell to WebAssembly using GHC's WASM backend and the Miso framework, so the entire proof checker runs locally in the browser with no server required.

---

Features

• Dynamically build proofs using the HTML5 Drag and Drop API.
• The checker highlights errors in your proof that you can fix afterwards.
• Highlight text and press '(' to enclose it in parentheses.
• Type aliases like 'forall' to get unicode characters (available aliases are shown in the sidebar).
• View the definitions of all rules of the current logic system in the sidebar, printed using MathJax.
• Look at exemplary proofs by clicking the corresponding buttons in the sidebar.
• Switch logics in the sidebar.
• Share proofs by sharing the current URL, since proofs are encoded as a ?proof= query parameter.

---

Demo

Visit the automatically hosted website at finch.vatthauer.xyz.

---

Documentation

Automatically generated haddock documentation is available at finch.vatthauer.xyz/docs.

---

Setup

Prerequisites

The recommended way to set up the development environment is with Nix. The flake.nix at the root of the repository provides a reproducible shell that includes the full WASM toolchain.

With Nix and flakes enabled, enter the development shell with:

nix develop .

Building

After Nix is installed, the project can be built with:

nix develop . --command bash -c "make"

The finished site lands in the public/ directory.

Running locally

make serve

This builds the project and then serves public/ using http-server.

Generating and Deploying the Documentation

Building the documentation requires a regular GHC installation without WASM, this is also provided using Nix:

nix develop .#test

To fully build and serve the app together with its documentation (which can be found in the sidebar of the website), run:

nix develop .#test --command bash -c "make haddock"
nix develop . --command bash -c "make serve"

Running Tests

You can run the test suite with:

nix develop .#test --command bash -c "make test"