Holbert: Reading, Writing, Proving and Learning in the Browser
summary
Holbert is a browser-based pedagogical proof assistant and online textbook platform that embeds editable proof exercises and rule definitions directly in pages, implemented in Haskell and compiled to JavaScript via GHCJS. It provides a video-game interface for natural-deduction proof trees, editable rule sets, lambda-term higher-order abstract syntax, pattern unification and induction tactics, equality rewriting and a prose-style case mode. It is working in classes (TU Dresden and an Australian use), but remains work-in-progress: missing sequent/substructural support, calculational notation and multi-document library imports. higher-order unification
AI-written summary · about
chapters (6)
related talks
42mLive-Coding Mathematics Your First Clojure Proof
01h 34mFormal Logic Undressed
34mLiquid Haskell: Verification with Refinement Types
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
46mRefinement Types from Light to Deep Verification
36mBarliman: trying the halting problem backwards, blindfolded
19mAutomated Verification of Fundamental Algebraic Laws
32mDon’t Call Us, We’ll Call You