Pre-RFC: Add a built-in support for totality (or non-panicking/aborting) asserting

[dead-claudia]

As more and more things get failable or fault-tolerant variants (I'm not even going to try to list them all), and as Rust finds its way into more stability-critical systems where any form of aborting or termination must be avoided at virtually all cost, it'd be incredibly helpful to have something similar to the often-used no_panic userland macro or its inspiration dont_panic built into the compiler.

There's benefits to this that simply cannot be done in userland:

1. The compiler could infer totality from the absence of any non-returning calls other than the (obviously unsafe) core::intrinsics::unreachable_unchecked(), and then use this to check even debug builds for this. The usual linker approach simply cannot do this.
2. The compiler could use its awareness of the call chain to pinpoint exactly where the non-returning call could lie, and in some cases recommend to the user possible alternatives.
3. By marking a function as total, the language server could know to constrain its suggestions to only callers known to panic. Interop with the type checker provides the server with the ability to hide panicking calls from the list of suggestions.
4. A compiler option could mandate that all functions in a given crate don't panic. This is useful for stability-critical crates as well as #![no_std] crates.

My first thought is maybe a total keyword with the following rules:

• All intrinsic functions returning ! or a no-variant enum type are considered non-total except for core::intrinsics::unreachable_unchecked()
• External calls returning ! or a no-variant enum type are considered non-total
• If validation of convergence of an expression depends on the expression's own totality, it's considered non-total.
  • This handles direct recursion, indirect recursion, and even Y combinators.
  • This check is also sufficient for detecting infinite loops.
• An expression is considered possibly-non-total if and only if it contains any non-total or possibly-non-total subexpression.
• A function is considered possibly-non-total if any statement within is possibly-non-total. Calls to it carry this same possible non-totality.
• The total modifier asserts the function is not possibly-non-total. And total { ... } blocks do the same for their inner statements. Keyword generics/effects/whatever-turns-out-to-be-used will be used to allow parameterization over this similarly to const.

---

There's admittedly still quite a bit of work to be done here for things like bounded iterators and array index access. Also, the programming style will admittedly start out very different than for typical Rust.

[RustyYato]

I don't think we can bolt on a termination checker onto Rust. That is use limited to proof assistants.
But the no unwind/abort subset of this proposal does seem useful. How would this interact with traits and generics? It would be a shame if this didn't compose.

[dead-claudia]

But the no unwind/abort subset of this proposal does seem useful. How would this interact with traits and generics? It would be a shame if this didn't compose.

@RustyYato That was my initial idea before I expanded it to cover other things. But even if those two are all it covers, it's fine by me.

[programmerjake]

please don't call it converging, that isn't the opposite of diverging as you seem to think, but instead commonly used for GPU code where you want all threads in a workgroup to go back to executing in lock-step at the end of a loop or conditional execution (threads are kinda faked by having one instance of your program per SIMD lane and converging is when all threads that have anything left to run are not masked off by some condition).

you are probably thinking of total, or maybe primitive recursive. LLVM uses willreturn nounwind, which is quite distinct from LLVM convergent.

To be pedantic, converging is the opposite of diverging in the sense of not having the GPU converging property, but that's not the meaning of diverging you mean by enforcing totality.

[dead-claudia]

@RustyYato @programmerjake Updated to use the math term "total" instead of "divergence" (as used to refer to the ! type) to make it clear what I mean. Sorry for the confusion.

Now if maybe software and computer engineering could stop creating ambiguity with math and science terms, that'd be nice... 😅

[kennytm]

... detecting infinite loops.

there are two kinds of "non-totality" (expressions with type !, excluding return/break/continue)

1. those that kills the execution: panic!(), abort(), exit(), infinite recursion (stack overflow) etc
2. those that causes the program to loop forever loop {}

practically the first case is much more "dangerous", since once you hit them you'll lose all your states; while for the second case you can still conduct some live debugging and recovery.

however, the proposed "totally" effect will only likely catch code using while loops (since without knowing the condition we must assume they can possibly loop forever), so I'm not very sure about using this new effect to detect "any form of aborting or termination".