5 ms·
You can always run model checkers like Kani, though even that is limited.
by PartiallyTyped 2y ago
You can always run model checkers like Kani, though even that is limited.
- medo-bear 2y agoSo no?
- johnisgood 2y agoThe answer is that it is not. It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now. (And a compiler being formally verified vs. being able to write formally verified code means two different things.)
- deleted 2y ago[deleted]
- medo-bear 2y agoI think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets
- johnisgood 2y agoAt this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.
- keybored 2y agoYou presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be). That seems excessive and tedious.
- medo-bear 2y agoThe point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems
- woodruffw 2y agoI don’t think Rust’s actual safety properties aren’t overhyped, although they may be subject to misunderstanding about their exact extent. Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.
- keybored 2y agoDouble negation makes things ambigious.
- woodruffw 2y agoThe second negation is a typo, but it’s too late to fix it.
- medo-bear 2y ago> although they may be subject to misunderstanding about their exact extent Isnt that what overhype means? Also no one is saying that Rust is unique in being overhyped. It is true of almost any language worth writing in, including c, lisp, python, haskell, type script etc.
- woodruffw 2y ago
- chillingeffect 2y agoRust is to safe as Tesla is to autopilot.
- medo-bear 2y agoAs Tesla is to Tesla
- mardifoufs 2y agoJudging by the facts, are you saying that Tesla has a safe auto pilot? Rare to see on HN :^)
- chillingeffect 2y agoHeh no... I was going for "the average person thinks Rust is automatically safe." And "the average person thinks Tesla is automatically safe."
- lambda 2y agoYou also need to consider that formal verification is not the be-all/end-all of correctness. Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Java LinkedList implementation that was buggy due to the formal model not taking into account integer overflow. There are parts of the Rust language and standard library that have been formally verified. That helps provide confidence that the basic model, of having safety properties upheld by unsafe core functions, to be sound. But the big advantage of Rust, especially for everyday open source code that the world widely depends on, is that it strikes a good balance between a language that people actually want to use, and which can provide good practical safety guarantees. Rust is far, far safer than C and C++. Most other memory-safe languages also are, but trade that off for lower performance, while Rust provides a similar level of performance as C and C++. And additionally, it's a language that people actually want to use for writing a lot of the core infrastructure. As far as I know, I have never use any open source software written in Ada/SPARK. People just don't do it. The only reason they generally do is if they need to for functional safety reasons, in a high-criticality system, and they find it easier to get their software certified by writing it that way. And even in safety critical systems, most people find using a subset of C, with restrictive rules, static checkers to check those, code review, and extensive testing, done by independent teams and testing on real hardware with requirements based tests that achieve 100% coverage at the MC/DC level is considered to be the gold standard of verification. Formal verification can not possibly provide some of the safety guarantees that testing on real hardware based on actual system level requirements can provide. Formal verification is one tool in a toolbox. It is useful for providing certain guarantees. But it's less important than many other factors for the actual improvements in safety that Rust can provide; by actually being used, in critical software that is exposed to potential network based exploitation, a memory-safe language like Rust makes a much better foundation than C or C++, and more people will actually use it in such a context than Ada/SPARK.
- medo-bear 2y agoThe article talks about compiling formalized C code to Rust. While interesting from a tinkering perspective, I fail to see any significant utility in safety, security, readability, popularity and ease of language. Can you please educate me as to what I am missing