I build small programming languages, theorem provers, and other systems related to PLT concepts.
I sometimes write about the things I learn βοΈ in my digital notepad π
The latest published post was a report on Propositions as Types β
Detour π π·
Detour is a small proof-checker for a mix of Second-order Propositional Logic and First-order Predicate Logic Natural Deduction proofs in Fitch-style notation.
It is a first step into the area of proof-checkers and (interactive) proof assistants. I picked the Fitch-style notation because I find it nice to look at. The goal is to have a very simple proof-checker that supports user-defined inductive data types/syntactic constructs, proof by induction, case analysis and maybe more.
An example proofβa proof of totality of the addition on natural numbers.