Verified software development in proof assistants

F* is one of the most interesting systems for this particular question.

Low* is explicitly designed to model C-like low-level computation. Its libraries model:

• stack allocation
• heap allocation
• C arrays
• machine integers
• C memory
• system-level C functionality

and KaRaMeL erases proofs before generating C (comparing to Why3 which can keep runtime asserts, if you need such ones).

Conceptually:

F*/Low*
    |
    | proofs specifications
    |
    v
verification
    |
    | erase proofs
    |
    v
Low-level implementation
    |
    v
    C
    |
    +--> stack
    |
    +--> heap
    |
    +--> explicit allocation
    |
    +--> no GC required

This is fundamentally different from:

high-level functional language
             |
             v
             C
             |
             v
    generated GC runtime

Low* is specifically trying to model the C memory behavior rather than hide it behind a tracing collector.

However, F* as a whole should not be labeled "no GC" bcs:

F*
 |
 +--> OCaml backend       -> OCaml GC
 |
 +--> F# backend          -> .NET GC
 |
 +--> Low*/KaRaMeL -> C   -> can be GC-free
 |
 +--> other backends      -> depends

So F* can be treated as "backend-dependent" classification.

Dafny is almost the opposite example. Supposing Dafny -> C++ it does not follow that you get "normal manual-memory C++". Dafny has its own runtime, support infrastructure, and generated C++ can depend on that infrastructure.

Therefore:

  Dafny
   |
   v
  C++
   |
   +--> Dafny runtime
   |      |
   |      +--> runtime representations
   |      |
   |      +--> collections
   |      |
   |      +--> memory management
   |
   v
program

The generated C++ can therefore effectively have managed-memory semantics even though C++ itself has no mandatory tracing GC.

Isabelle's code generator produces SML, OCaml, Haskell and Scala.

Therefore the memory-management story is inherited largely from the target:

Isabelle/HOL
 |
 +--> SML      -> SML runtime/GC
 |
 +--> OCaml    -> OCaml GC
 |
 +--> Haskell  -> GHC GC
 |
 +--> Scala    -> JVM GC

So Isabelle doesn't need an its own "Isabelle GC", but the generated program is certainly not necessarily GC-free.

Agda is similar:

Agda
 |
 +--> Haskell     -> GHC GC
 |
 +--> JavaScript  -> JS engine GC

Lean is different.

Lean's executable model includes a runtime system, and its compiler targets native code through its compilation infrastructure.

A more accurate model for Lean is:

    Lean
     |
     v
Lean compiler
     |
     v
native code
     |
     +--> Lean runtime
              |
              +--> runtime representations
              |
              +--> memory management
              |
              +--> GC/runtime machinery

ACL2's ATC is interesting because it generates C and is explicitly designed as a proof-generating C code generator.

The conceptual model is:

       ACL2
        |
        | proof
        |
        v
       ATC
        |
        v
        C
        |
        v
ordinary C compiler

ATC is much closer to: "generate C that follows the proved semantics" than to: "generate C plus a large managed-language runtime".

So GC is not normally intrinsic for ACL2.

Of course, nothing prevents the generated C program from linking against a GC library if the application requires one.

Vale operates at a much lower level - Vale is a DSL/toolchain for verified ASSEMBLY (ARM, x86?) for F* and Dafny, see more. The project today does not look as too alive though.

Its generated/verified code can be incorporated into systems software without a mandatory tracing GC.

But, just as with C or assembly generally:

"no mandatory GC"
       !=
"GC impossible"

You can implement a GC in assembly.

The relevant question is whether the Vale-generated code requires one. Normally, no.

HOL4 can generate SML, so its extracted code uses GC of SML (not specially generated by HOL4).

There are actually 3 independent axes:

                       GENERATED PROGRAM
                              |
             +----------------+----------------+
             |                                 |
          managed                          explicit
             |                               memory
             |                                 |
       +-----+-----+                    +------+------+
       |           |                    |             |
      GC       RC/other              malloc,       ownership,
       |                              free         regions
       |
       v
runtime support

So "GC or no GC" is not the whole story.

For systems programming, this it a richer classification:

This is why the CertiCoq ecosystem is particularly interesting.

It is possible to have:

               Rocq
                 |
           proof/program
                 |
             CertiCoq
                 |
                 v
             generated C
                 |
        +--------+--------+
        |                 |
   application        verified GC
        |                 |
        +--------+--------+
                 |
                 v
           machine code

So there is nothing contradictory about:

      "C code"
         +
"garbage collection"
         +
"formally verified"

C doesn't prohibit GC; it simply doesn't provide one as part of the language.

Reduce the enormous table:

So, yes: there absolutely are provers/formal-verification systems where the generated language is C/C++ but the resulting program can still have a garbage collector.

The cleanest conceptual distinction is:

                   C/C++
                     |
          +----------+----------+
          |                     |
       GC-based             GC-free
          |                     |
   runtime/collector       malloc/free
          |                 ownership
          |                  regions
          |                  arenas
          |                     |
   CertiCoq-style         Low*/KaRaMeL
   / Dafny-style             Why3/C
                            ACL2/ATC

CertiRocq-generated code normally relies on a CertiRocq runtime, and that runtime includes a generational garbage collector.

See: "Memory Model and Garbage Collection - CertiRocq"

And: "Certifying graph-manipulating C programs via localizations within data structures"