no-panic

kewise, SPARK (and C++, for that matter) is capable of things that Rust is not. > The type system in Rust, Ada, and C++ are all robust enough at least to accomplish this. I'm not sure about that? You might be able to approach what SPARK could do, but at least off the top of my head you'll need to make a check the compiler can't verify somewhere. And that's just for this instance; I don't think Rust nor C++ are able to match SPARK's more general capabilities. For example, I believe neither Rust nor C++ are able to express "this will not panic/throw" in their type systems. There are tricks for the former that approximate the functionality (e.g., dtolnay/no_panic [0]), but those are not part of the type system and have limitations (e.g., does not work with panic=abort). The latter has `noexcept`, but that's basically semantically a try { } catch (...) { std::terminate(); } around the corresponding function and it certainly won't stop you from throwing or calling a throwing function anyways. > Exactly! This is the root of my issue: you can accomplish this magical "proof" you speak of without using SPARK or Ada or any special "contract" language. Perhaps I wasn't clear enough. I was trying to say that it's contradictory to complain about formal proofs while also claiming you can accomplish the same using other programming languages' type systems because those type systems are formal proofs! It's like saying "You don't need formal proofs; just use this other kind of formal proofs". I don't think that assertion is correct either. The reason separate languages are used for this kind of proof is because they restrict operations that can't be proven, add constructs that provide additional information needed for the proof, or both. Perhaps as an extreme example, consider trying to make compile-time proofs for a "traditional" dynamically-typed language - Smalltalk, pre-type-hints Python, Lua, etc. [0]: https://github.com/dtolnay/no-panic

unwrap()/etc. would seem "harder" to write/justify than the alternative. The main exception I can think of are more one-off cases where the author is intentionally sacrificing robust error handling for the sake of speed/convenience, but that's a more language-agnostic thing that pretty much "doesn't count" by definition. > I hope this philosophy do not reach the Linux kernel. IIRC this is being worked on, especially given Linus's position on panics in the kernel. [0]: https://github.com/dtolnay/no-panic

attern match on a.get(x) doesn't help because if it's ever None (and your program logic expects that x is in bounds) then you are kind of forced to bail. The downside here is that we aren't catching this bug at compile time. And it's true that sometimes we can rewrite the program to not have an indexing operation, usually using iterators (eliding the bounds check will make the program run faster, too). But in general this is not possible, at least not without bringing formal methods. But that's what tests are for, to ensure the correctness of stuff type errors can't catch. Now, there are some crates like https://github.com/dtolnay/no-panic or https://github.com/facebookexperimental/MIRAI that will check that your code is panic free. The first one is based on the fact that llvm optimizations can often remove dead code and thus remove the panic from a[x] or a / b - if it doesn't, then compilation fails. The second one employs formal methods to mathematically prove that there is no panic. I guess those techniques will eventually be ported to the kernel even if panics happen differently there (by hooking on the BUG mechanism or whatever)