Panic bounds in the type system level for guaranteeing panic-free code

I'm going to have details on this somewhat soon :eyes: Right now I've experimented with deranged to the extent the compiler allows. If I use generic_const_exprs, the door is opened to a lot of things. The main thing compiler integration is needed for is for values that don't neatly fit within a single type (200u8 + 100u8, for example).The compiler could choose the representation automatically.

I think it would be great to have an infinite-precision integer type that's only usable at compile-time. Then people can avoid needing to pick particular types in generic parameters when there's no particular one that makes sense. (Array lengths staying usize still makes sense, of course.)

Then yeah, compiler support into the backend so LLVM can handle it smartly would be particularly cool.

First thing is to get finite-precision values in general, namely those that fit in u128/i128.

1 Like

Sorry, I’m late to the game: I think the previous discussion — interesting as it may be on a type level — misses a crucial point. When going for something absolute like “panic-free”, we should note that whatever properties the Rust type checker can prove about some program, this program can still fail because the assumed evaluation semantics of the language are not provided by the real execution environment. For example, stack and heap size are both limited. In the latter case, we could flag all possible allocations as potentially panicking, which would limit the usefulness of this rather intrusive feature to a tiny subset of all usage. In the former case, we have no such possibility.

In my opinion, writing code that “must not ever fail” can only be done in a total language. The result is then run on proven deterministic infrastructure. To my knowledge, none of these are goals of the Rust ecosystem.

I agree that such guarantees are outside of Rust's purview. I call the services like this "bulletproof" because, while it is fine against "small arms fire", it is definitely not immune to larger things like power cuts, network deliverability issues, and root access to the host machine.

Personally, I think something like panic=disallow where the linker makes sure that no panic hook calls are made would be sufficient (though it leaves it to the linker rather than the compiler), but I also have only needed "bulletproof" guarantees, not "life-threatening" levels. Given that the latter does exist and uses languages less strict than Rust, I feel like there are development practices and patterns that can be employed for Rust as well even without sweeping new-marker-trait changes to the language itself.

2 Likes

To me, there is value in verified panic-free code not specifically for guarantees of run-time reliability, but rather to know that I have successfully written a total function, a function that has no unaccounted-for edge cases where it would panic.

Of course this is not a guarantee of correctness, because it doesn't exclude stack overflow, infinite loops, or returning the wrong answer. But reducing the number of cases one needs to consider to evaluate whether code is correct is, in general, something Rust already does a lot of (such as memory safety and default non-nullable pointer types) and thereby provides value to its users.

It may still be too impractical to actually work under such a restriction, of course. But note that the popular examples of difficulty of eliminating panic branches are indexing and arithmetic — and there are plenty of functions that contain no indexing or arithmetic.

(Perhaps I should try programming with no_panic - Rust and see how bad it is…)

8 Likes

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.