Colouring Flags with Dafny & Idris
summary
Compares Dafny’s imperative design-by-contract + Hoare/Boogie pipeline with Idris’s dependently typed, type-driven approach by reimplementing the Dutch National Flag (filter/merge examples) in both languages, showing a concrete Idris implementation that builds correctness into types and uses typed holes for synthesis, versus Dafny’s separate specs, runtime-versus-compile erasure tradeoffs and use of ghost variables. Notes practical differences: Idris compiles correctness from a tiny core, Dafny calls external tools, and the verification artifacts can be either runtime relevant or erased.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 2:09Motivation for Dafny vs Idris
- 3:17Verification spectrum
- 4:02Idris features
- 5:28Quantitative typing
- 6:09Direct comparison Dafny vs Idris
- 8:39Dutch flag problem choice
- 9:43Dutch flag and insertion sort
- 10:49Idris approach to the Dutch flag problem
- 11:31Dependent types
- 13:37Idris filter function
- 14:41Type-driven proofs
- 15:22Code as spec Idris vs Dafny
- 16:03Efficiency and ghost vars
- 17:07Verification pipelines
- 17:49Interactive editing
- 18:10Future work
related talks
47mType-Driven Development in Idris
41mType-driven Development of Communicating Systems in Idris
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
41mFun With Categories
51mFunctional Programming and Domain Driven Design - a match in Heaven!
51mStretching the Glasgow Haskell Compiler: Nourishing GHC with Domain-Driven De...
34mHow I learned to stop worrying and love Functional Design
49mFunctional Design Explained