The Cogent and Dargent approach to facilitating verified software development
summary
Cogent is a restricted functional language with a linear type system and a certifying compiler that emits C, getter/setter code and Isabelle/HOL refinement proofs; two journaling file systems compile to ~4k lines of Cogent plus ~2k C, run within ~10% of handwritten C, and cut manual verification effort from seL4’s 1.65 to about 0.38 person‑months per 100 lines — roughly two‑thirds less work. Dargent is a data‑layout spec language that generates bit‑level C accessors, verifies layout/type correspondence, and eases driver proofs (tiny timer, power control).
AI-written summary · about
chapters (19)
- 0:00Introduction
- 1:06Motivation for verified systems software
- 3:16Challenges in verification
- 6:07Cogent and Dargent projects overview
- 8:35Cogent language design
- 11:46Linear types in Cogent
- 17:50Compiler output proofs
- 21:21Cogent file systems results
- 23:09Limitations and Dargent intro
- 26:00Data layout challenges
- 29:35Dargent language features
- 35:22Compiler certificates and C code
- 37:14Verifying layout and types
- 41:48Dargent results and apps
- 46:11Future directions
- 51:56Project availability
- 52:40Q&A 1
- 57:19Q&A 2
- 1:03:38Q&A 3
related talks
01h 04mCoq's vibrant ecosystem for verification engineering
21mMechanised Hypersafety Proofs about Structured Data
01h 02mLanguage Design meets Verifying Compilers
01h 28mA Galilean revolution for computing
27mC4: verified transactional objects
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems