literate-programming #ebook developing the proof assistant "Proust" in Racket, apparently written for teaching Waterloo's Logic and Computation course, with an overview of propositional and predicate #logic, as well as #Coq and #Agda. #cc by-nc-sa
on 02021-02-09a presentation of a compiler that emits code along with its proof in #Agda, which I guess is a sort of proof assistant? With live Agda code in a page. #formal-methods #compilers
on 02015-11-16