Faux Type Theory: Three Minimalist Ocaml Simple Proof Checker Implementations
Posted4 months agoActive4 months ago
github.comTechstory
supportivepositive
Debate
10/100
OcamlProof AssistantsType Theory
Key topics
Ocaml
Proof Assistants
Type Theory
Andrej Bauer shared a GitHub repository with three minimalist OCaml implementations of a simple proof checker, sparking a low-key discussion.
Snapshot generated from the HN discussion
Discussion Activity
Light discussionFirst comment
10s
Peak period
1
0-1h
Avg / period
1
Key moments
- 01Story posted
Sep 13, 2025 at 2:33 AM EDT
4 months ago
Step 01 - 02First comment
Sep 13, 2025 at 2:33 AM EDT
10s after posting
Step 02 - 03Peak activity
1 comments in 0-1h
Hottest window of the conversation
Step 03 - 04Latest activity
Sep 13, 2025 at 2:33 AM EDT
4 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
ID: 45229828Type: storyLast synced: 11/17/2025, 2:02:13 PM
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
https://mathstodon.xyz/@andrejbauer/115191725004191889
> This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at:
https://github.com/andrejbauer/faux-type-theory
> The repository has three minimalist OCaml implementations of a simple proof checker:
> 1. A basic one showing how to implement bidirectional type checking and type-directed equality checking, using monadic style programming.
> 2. An extension with rudimentary holes (meta-variables) and unification.
> 3. A version that implements "variables as computational effects", using native OCaml 5 effects and handlers.