• toastal@lemmy.ml
    link
    fedilink
    arrow-up
    1
    ·
    edit-2
    1 month ago

    Correct me if I am wrong, but my understanding is that you use Coq to prove your theroem, then need to rewrite it in something else. I think there is some OCaml integration, but OCaml—while having create performance for a high level language & fairly predictable output—isn’t well-suited for very low-level kernel code. The difference in the ATS case (with the ML syntax similarity 🤘) is you can a) write it all in a single language & b) you can interweave proof, type, & value-level code thru the language instead of separating them; which means your functions need to make the proof-level asserts inside their bodies to satisfy the compiler if written with these requirements, or the type level asserting the linear type usage with value-level requirements to if allocating memory, must deallocate memory as well as compeletly prevent double free & use after free.

    For those in the back: Rust can’t do this with its affine types only preventing using a resource multiple times (at most once), where linear types say you must use once & can only use once.

    • ☆ 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.