4 ms·
Yes, I've seen this comment a number of times now. ATS is a very interesting language! But there are a wide range of options for formal verification of systems
by ekidd 6y ago
Yes, I've seen this comment a number of times now.
ATS is a very interesting language! But there are a wide range of options for formal verification of systems programs, including the techniques used for the formally verified seL4 kernel, ATS, recent Ada work, TLA+, etc. Some of these tools have been very successful for certain projects.
But the more powerful proof systems involve tradeoffs. Frequently, you need to invest significant amounts of developer effort in exchange for very rigorously proven code. I've played with a number of these systems over the years, and they're great. But the costs would be hard to justify for many projects.
Rust occupies a slightly different niche. It focuses on preventing several classes of memory errors and data races. It's certainly harder to learn than Python, but probably easier than some common subsets of C++.
So the right tool for the job depends on what you're trying to do. If you want to formally verify your kernel's security model, or your distributed protocol, Rust would be a poor choice. If you want a language that makes it easy to work within sight of the metal, and that takes pains to make expensive operations visible, Rust can be a reasonable choice.
- deleted 6y ago[deleted]
- ghostwriter 6y agoI agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether or not a suggested amount of effort to bring Rust into existing and well-established C codebase is a great idea and is justified on a technical merit basis, compared to the effort of brining more sophisticated formal proof assistants that aim at non-intrusive interfacing with C while being productive for the cause of promoting safe and formally-verified programming. Python's gradual typing with MyPy demonstrated a great utility of static type checking that could be brought to existing project through many small and non-desruptive iterations. From my observation an learning of ATS, I expect even greater utility of gradual formal proofs that ATS enables for C. There are tons of successful C codebases, they are used in production around the world and contain a great amount of battle-tested knowledge. They just miss formal proofs that now could be gradually written for them.