8 ms·

Why not just use a verifiable subset of C? https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html

• aeneasmackenzie 2y ago
  Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.
  • LiamPowell 2y ago
    There's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick SPARK any day. Having a rich type system and not having to work with pointers makes proving a program so much easier.
    • MaxBarraclough 2y ago
      Right, Frama-C can formally prove properties of C code. There are also proprietary solutions that do something similar: • https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php • https://www.trust-in-soft.com/ https://www.trust-in-soft.com/