You Got Your Idris in My C++! A First Look at Denotational Design
summary
Argues that designing meanings in Idris and then translating to C++11 yields tighter, simpler APIs and verifiable invariants. Shows concrete tooling (Idris REPL, Boost optional), implements length-indexed vectors and an addition proof that compiles as a proof and rejects broken implementations, and rethinks an audio API as time→loudness functions translated into C++ templates. Outcomes: worked examples, machine-checked proofs for properties, and practical C++ patterns—useful if wanting formal checks without abandoning C++/Java/Agda workflows.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 1:58How can we sneak the fun languages in
- 4:05What is Denotational Design
- 4:45Haskell
- 5:28Idris
- 6:01Idris Example
- 6:39Dependent Types
- 7:25Dependent Values
- 12:23Natural Numbers
- 12:56Syntax
- 14:39Proofs
- 16:45Program Proof
- 17:30Review
- 20:05Base Case
- 22:55Inductive Case
- 27:26Applying Denotational Design
- 28:54C API Example
- 31:19What is an Idris
- 37:27Happy Warm Feelings
related talks
53mCan C++ Data-oriented-design be Improved?
05mIdris (Lightning Talk)
01h 28mData-Oriented Design and C++
01h 03mWriting sustainable software. The how and the what!
01h 02mRust/C++ Interop: Carcinization or Intelligent Design?
40m"Fine-Grained C++ Interop"
31mFrom C++ APIs to Idiomatic Rust: Wrapper Design Patterns
01h 55mThe next big Thing