Comments (4)
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.
from magmide.
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 :)
from magmide.
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.
from magmide.
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.
from magmide.
Related Issues (17)
- Build magma on a subset of an existing language HOT 5
- Enable github discussions? HOT 1
- Typos in `intro-verification-logic-in-magmide.md` HOT 1
- Please add a donate button HOT 1
- Comparison with TLA+ HOT 4
- Can you evaluate ATS? HOT 1
- Research debt for contributors HOT 1
- Avoid Sisyphus trap HOT 2
- Building the community HOT 4
- wtf is this and how will it make my life easier? HOT 2
- Comparison with B-Method and Rodin HOT 4
- Great project HOT 2
- Basil - same syntax, same computational power in compile-time as in runtime HOT 7
- consider name? HOT 8
- Thoughts (if you *truly* wish to make this a practical language) HOT 4
- The "Coq Coq Correct" link is broken on the README
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from magmide.