4 ms·

Does Agda provide tools for program extraction? I'm curious where the state of the art is for using proof checkers/dependently typed programming languages to de

by bcoates 12y ago

Does Agda provide tools for program extraction? I'm curious where the state of the art is for using proof checkers/dependently typed programming languages to derive correct-by-construction programs in lower-level languages like C.

thoughtpolice 12y ago
Agda has a compiler that can extract Haskell or JavaScript, yes. But Agda doesn't seem to be very heavily used for this purposes - Coq on the other hand seems to have very mature extraction capabilities for Haskell/OCaml/Scheme and has been used quite a bit for this purpose. You could also of course use Idris, which directly compiles to executables.
- steveklabnik 12y ago
  Or ATS, which compiles to C.