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

    If you believe in ADTs, limiting mutation, & a type system that goes beyond Rust’s affine types + lack of refinements (including a interleaved proof system), you could be writing kernel code in ATS which compiles to C.

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