• ☆ Yσɠƚԋσʂ ☆@lemmy.ml
    link
    fedilink
    arrow-up
    2
    ·
    1 month ago

    You’r right that only OCaml and Haskell can be used as extraction target for Coq programs. However, it is possible to use Coq to write verified C software. On example is the Verified Software Toolchain that lets you translate C programs to a format that Coq understands and can prove theorems regarding their behavior.