Certified Programming with Dependent Types
by Adam Chlipala · first published 2013
81% recommend19% neutral
Why HN recommends it
Practical, engineering-focused Coq textbook on building programs with proofs of correctness, using dependent types and proof automation. Suits readers who have finished Software Foundations and want advanced practice.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
Little Prover
Daniel P. Friedman, Carl Eastlund, Duane Bibby
Recommended by 9 · mentioned by 189 recommend · 18 mention9 recommend · 189 recommend
Software Foundations
Benjamin C. Pierce
Recommended by 58 · mentioned by 6058 recommend · 60 mention58 recommend · 6058 recommend
2010–2026Proofs and types
Jean-Yves Girard
Recommended by 6 · mentioned by 106 recommend · 10 mention6 recommend · 106 recommend
2010–2022Programming Scala
Dean Wampler, Alex Payne
Recommended by 9 · mentioned by 259 recommend · 25 mention9 recommend · 259 recommend
2013–2026Functional Programming In Scala
Paul Chiusano
Recommended by 33 · mentioned by 5333 recommend · 53 mention33 recommend · 5333 recommend
2013–2023Functional JavaScript
Michael Fogus
Recommended by 25 · mentioned by 3025 recommend · 30 mention25 recommend · 3025 recommend
2013–2026Practical Foundations for Programming Languages
Robert Harper
Recommended by 17 · mentioned by 2717 recommend · 27 mention17 recommend · 2717 recommend
2008–2026Types and Programming Languages
Benjamin C. Pierce
Recommended by 132 · mentioned by 226132 recommend · 226 mention132 recommend · 226132 recommend
For learning this sort of thing I always recommend Pierce's Software Foundations [0] and Chlipala's Certified Programming with Dependent Types [1] which are both available online for free, but I'm also reading through Coq d'Art as well and like it a lot... unfortunately it's harder to find. [0] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html…
on “Coq: The world’s best macro assembler? (2013) [pdf]” ↗If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]). His book "Certified Programming with Dependent Types" is a fantastic resource. Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language…
on “Coq to Rust Program Extraction” ↗I'd say it's the recommended book for type systems. For type theory, I'd recommend "Certified Programming with Dependent Types" by Adam Chlipala or "Programming Language Foundations in Agda" by Philip Wadler.
on “Types and Programming Languages (2002)” ↗FWIW, I'm not mathematically-inclined and haven't found Coq to be painful to use. As soon as I really want verified code, doing stuff in Coq seems like the easiest path because the proof automation tooling is pretty great, especially if you follow the approach in Certified Programming with Dependent Types[0]. I also like Alloy[1] for messing around with logical data structure definitions interact
on “Verified Programming in F*: A Tutorial” ↗If you really want to build on "rock", check out Bedrock: http://plv.csail.mit.edu/bedrock/ . Don't just prove your program is memory safe, prove it satisfies arbitrary properties! (A bit tongue in cheek, but the tools are really cool). Check out http://adam.chlipala.net/cpdt/cpdt.pdf for a nice introduction.
on “Building on Rock, Not Sand” ↗If you want to get started with Coq there are two good resources. One is Software Foundations[sf] by Benjamin Pierce. There's also Certified Programming with Dependent Types[cpdt] by Adam Chlipala. I would say [cpdt] is more advanced than [sf], so I think it's best to start with [sf] and then start on [cpdt] if you feel up for the challenge. I have mixed feelings about Coq as a tool for software
on “Formal Methods of Software Design: an online course by Eric Hehner” ↗At this point, the standard intro text is Software Foundations [1]. I highly recommend it; it will teach you Coq and also probably make you a better programmer. After SF, Certified Programming with Dependent Types [2] gets more into the practice of proving serious programs correct. These books are both available online in the form of literate Coq files. As far as online lectures, OPLSS [3] often
on “Proof of linearizability in Raft using Coq” ↗You are incorrect. Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. If you want to read more about this subject, I recommend Adam Chlipala's "Certified Programming with Dependent Types": http://adam.chlipala.net/cpdt/
on “Blue. No, Yellow” ↗Well, very indirectly, in the sense that OCaml hackers will think alike to some extent, and all languages involved have strong types. But otherwise not very much. This is producing implementation code. Basically, this is program synthesis via dependent types. See http://adam.chlipala.net/cpdt/ for a deep dive into this concept; program extraction is introduced in the first chapter past the introd
on “Coq to Rust Program Extraction” ↗There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.
on “The Dawn of Formalized Mathematics” ↗Check out http://adam.chlipala.net/cpdt/
on “A formalization in Coq of the Haskell pipes library” ↗Benjamin Pierce has a course on the mathematical theory of programming languages, using the Coq Proof Assistant: http://www.cis.upenn.edu/~bcpierce/sf/toc.html Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof au
on “Why Lisp is a Big Hack (And Haskell is Doomed to Succeed)” ↗Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through. In a sense, a properly typed program provides a pro
on “As Math Grows More Complex, Will Computers Reign?” ↗…"has no impact". But on the other hand, I think studying dependent types is a fantastic way to get some perspective as an intermediate to advanced Haskell or OCaml programmer. Software Foundations and Certified Programming with Dependent Types are both great books to read. HoTT won't be on that list for some time if ever, but once you've got a good mental model for dependent types it's illuminating to see them worked out "from scratch" as…
on “Functional programming books review” ↗Have you looked at Adam Chlipala's Certified Programming with Dependent Types book? It uses Coq and Proof General. There's an online version: http://adam.chlipala.net/cpdt/
on “Software Foundations” ↗