No-Panic Rust: A Nice Technique for Systems Programming

>and the compiler will prove to you that your functions are upholding the invariants

From the article and only vague background Rust knowledge, I'm under the impression that the opposite is true: the compiler does not prove that. Hence why it's "assert_unchecked" - you are informing the compiler that you know more than it does.

You do get panics during debug, which is great for checking your assumptions, but that relies on you having adequate tests.

This isn't quite the same, but it reminds me of something a bit less clever (and a lot less powerful) I came up with a little while back when writing some code to handle a binary format that used a lot of 32-bit integers that I needed to use for math on indexes in vectors. I was fairly confident that the code would never need to run on 16-bit platforms, but converting from a 32-bit integer to a usize in Rust technically is considered fallible due to the fact that you can't necessarily assume that a usize is more 16 bits, and frustrating `usize` only implements `TryFrom<u32>` rather than conditionally implementing `From<u32>` on 32-bit and 64-bit platforms. I wanted to avoid having to do any casting that could silently get messed up if I happened to switch any of the integer types I used later, but I also was irrationally upset at the idea of having to check at runtime for something that should be obvious at compile time. The solution I came up with was putting a static assertion that the target pointer width was either 32 or 64 bits inside the error-handling path, followed by marking the code path as `unreachable!()` that would never get executed (because either the error handling path wouldn't be taken, or the static assertion would stop the code from having been compiled in the first place. Even though this wasn't meaningfully different from just conditionally compiling to make sure the platform was suitable and then putting `unreachable!()` unconditionally in the error handling path, having the compile-time insertion locally in the spot where the error was being handled felt like I magically turned the runtime error into a compile-time one; it was quite literally possible to write it as a function that could be dropped into any codebase without having to make any other changes to ensure it was used safely.

For systems where correctness is actually important, not just a nice-to-have (in most systems, it's nice-to-have,) we have had an increasing number of options over the years.

From tools like "spin" and "tla+" to proof assistants like Coq to full languages like Idris and Agda.

Some of the stronger-typed languages already give us some of those benefits (Haskell, OCaml) and with restricted effects (like Haskell) we can even make the compiler do much of this work without it leaking into other parts of the program if we don't want it to.

While I would love this to be true, I'm not sure that this design can statically prove anything. For an assert to fail, you would have to actually execute a code sequence that causes the invariant to be violated. I don't see how the compiler could prove at compile time that the invariants are upheld.

Sometimes the program is in an invalid state. You don't want to keep running the program. Better to fail spectacularly and clearly then to fail silently and try to hobble along.

At least sources of panic! are easily greppable. Cutting corners on error handling is usually pretty obvious

While sure, more things could be baked as results, most of the time when you see a panic that's not the case. It's a violation of the callee's invariants that the caller fucked up.

Essentially an error means that the caller failed in a way that's expected. A panic means the caller broke some contract that wasn't expressed in the arguments.

A good example of this is array indexing. If you're using it you're saying that the caller (whoever is indexing into the array) has already agreed not to access out of bounds. But we still have to double check if that's the case.

And if you were to say that hey, that implies that the checks and branches should just be elided - you can! But not in safe rust, because safe code can't invoke undefined behavior.

I personally would have used the assume crate but I guess this got standardized more recently. They call out the safeness requirement and that it’s a sharp edge but like you I think they understate the sharpness and danger.

Rust doesn't want to add any proof-system that isn't 100% repeatable, reliable, and forwards compatible to the language. The borrow checker is ok, because it meets those requirements. The optimizer based "no panic" proof system is not. It will break between releases as LLVM optimizations change, and there's no way to avoid it.

Trying to enforce no-panics without a proof system helping out is just not a very practical approach to programming. Consider code like

    some_queue.push_back("new_value");
    process(some_queue.pop_front().unwrap());

Or consider code like

    let mut count: usize = 0;
    for item in some_vec {
        // Do some stuff with item
        if some_cond() {
            count += 1;
        }
    }

Or so on.

Basically every practical language has some form of "this should never happen" root. Rust's is panics. C's is undefined behavior. Java's is exceptions.

Finally consider that this same mechanism is used for things like stack overflows, which can't be statically guaranteed to not occur short of rejecting recursion and knowledge of the runtime environment that rustc does not have.

---

Proof systems on top of rust like creusot or kani do tend to try to prove the absence of panics, because they don't have the same compunctions about not approving code today that they aren't absolutely sure they will approve tomorrow as well.

The standard library is slowly adding non-panicking options. The article shows some of them (like vec.push_within_capacity()) and ignores some others (vec.get_unchecked()). There is still a lot of work to do, but it is an area where a lot of work gets done. The issue is just that a) Rust is still a fairly young language, barely a decade old counting from 1.0 release, and b) Rust is really slow and methodical in adding anything to stdlib because of how hard/impossible it is to reverse bad decisions in the stdlib.

The same article written a couple years in the future would look very different

What I would like to see is a reliable distinction of different types of panics. In the environments where software I write is typically run, panics due to heap allocation failure are generally acceptable and rarely an indication of fragility. (By the time a heap allocation failure occurs, the computer is probably already thrashing and needs to be rebooted.) On the other hand, other kinds of panics are a bad sign. For example, I would frown on any library that panics just because it can't reach the Internet.

In other environments, like embedded or safety-critical devices, I would need a guarantee that even heap allocation failure can not cause a panic.

I would say that you are using them incorrectly if you assume them as recoverable. You should make everything you can so that they never happen.

However, since it is still possible to have them in a place where the exiting the process is not okay, it was beneficial to add a way to recover from them. It does not mean that they are designed to be recoverable.

> this is where most of it's overhead comes from

Overhead comes from the cleaning process. If you don't clean properly, you might leak information or allocate more resources than you should.

Author here -- that is surprising. What browser/OS are you on? I haven't had anyone else report this problem before.

This happened to me too (Safari on iOS).

Here’s a archived link:

https://web.archive.org/web/20250204050500/https://blog.reve...

Same, the web view in my Android client crashed after a couple seconds.

> This makes me wonder: are there any formal specifications on the complexity of this "optimizer as theorem prover"?

Basically, the promise here "We formally promise not to promise anything other than the fact that optimized code should have 'broadly' the same effects and outputs as non-optimized code, and if you want to dig into exactly what 'broadly' means prepare to spend a lot of time on it". Not only are there no promises about complexity, there's no promises that it will work the same on the same code in later versions, nor that any given optimization will continue firing the same way as you add code.

You can program this way. Another semi-common example is taking something like Javascript code and carefully twiddling with it such that a particular JIT will optimize it in a particular way, or if you're some combination of insane and lucky, multiple JITs (including multiple versions) will do some critical optimization. But it's the sort of programming I try very, very hard to avoid. It is a path of pain to depend on programming like this and there better be some darned good reason to start down that path which will, yes, forever dominate that code's destiny.

Compilers can typically reason fairly well about tail recursion like this. In this case the compiler cannot remove the assertion because you could pass in 0. But if you change the assert to be a >= 0 (which is vacuously true, as the warning indicates) it will optimize the code to "return 1" and eliminate the recursive call: https://godbolt.org/z/jad3Eh9Pf

The standard library has a significant amount of code that panics, so a `no_panic` crate attribute would currently only work for crates that don't depend on the standard library. I imagine most interesting crates depend on the standard library.

You could do it, but I would prefer guarantees on a per-call chain basis using a sanitizer. It should be quite easy to write.

As the author mentions, `panic!` is also not an acceptable failure mode in some applications. If you're developing safety-critical software and a process stopping is part of your risk analysis, many frameworks will ask you about the frequency of that happening. In that analysis, you may be required to set all systematic contributions to that frequency to zero. This happens, for example, if you try to control the associated risk using redundancy. If there is a code path that may panic, you may not be able to do this at all as you maybe just cannot conclude that your code does not panic systematically.