Thoughts on Frama C?

[Hirrolot]

Frama C is a project aimed at formally verified C code. With its weakest precondition calculus, it's possible to state assertions about C code that can be formally checked.

Since you're attempting to make a formally verified systems programming language, I'm curious what are your thoughts on it, since that's exactly what it does.

[blainehansen]

There are many projects that achieve the instrumental goals of Magmide, so it's likely Frama C does so (I don't have time to dig into it deeply now, but will at some point).

Magmide isn't just about instrumental goals though, it's about social goals, making verification sufficiently integrated and thoughtful and well-designed that it's actually attainable for working engineers, not just academics. My casual look at Frama C suggests it's still relying on Coq proofs? If that's the case it's not yet where Magmide wants to go, but of course it looks much more complete! People should take a look at it if it solves their more urgent goals :)

Please start a discussion rather than issues for questions like these :)

[Hirrolot]

Frama C is being used by engineers and not only academics; e.g., if memory serves me correctly, there was a bootloader formally verified with Frama C, and some other stuff from the industry. It doesn't rely on Coq proofs, since you just describe your set of expectations as preconditions, invariants and postconditions in the comments.

[AllanBlanchard]

Magmide isn't just about instrumental goals though, it's about social goals, making verification sufficiently integrated and thoughtful and well-designed that it's actually attainable for working engineers, not just academics.

Frama-C is used on industrial use cases for a long time. For an example of a recent work THALES has achieved CC EAL6 certificate for a JavaCard machine (https://link.springer.com/chapter/10.1007/978-3-030-90870-6_23) and more recently CC EAL7 (https://www.ssi.gouv.fr/entreprise/certification_cc/multiapp-v5-0-java-card-virtual-machine/) using Frama-C + its WP plugin. Most of the proofs (99%) are done automatically using SMT solvers.

[blainehansen]

I think your two comments reveal exactly what I'm pointing to as the problem. I should have been more precise, it's not that Magmide's goal is to bring "verification" in the abstract to working engineers, but full verification, the kind that can't be done mostly with an SMT solver and requires a proof assistant. Magmide intends to be a full proof assistant! But one that's designed to be used alongside production software (probably mostly systems software, but still). My problem is that when most academic-adjacent verification folks hear "verification for engineers" they think "fully automated tool", rather than a proof assistant that's designed and explained properly!

I took some time to skim through the tutorial pdf, and it seems Frama C mostly falls in the "not logically maxed out" category. I appreciate that Coq and other tools can be used when needed, but that's the entire point of Magmide, Coq isn't good enough! Magmide intends to be to Coq/LLVM what Rust is to C. It seems to me at this point that Frama C is to C what Flux or RustHorn is to Rust.

SMT solvers and decidable reflective proofs will obviously be a critical part of a successful verification language. But I won't be happy until working engineers are proving properties as ambitious as the memory safety of complex uses of unsafe. SMT solvers aren't going to make that happen, and my belief that working engineers are both capable and willing to do that kind of work (if the path isn't hopelessly shrouded in pointless research debt) is what it seems truly differentiates Magmide's goals from those of other projects.

Of course Magmide hasn't actually achieved anything useful yet! I wish I could make faster progress. In the meantime Frama C is infinitely more useful than Magmide.