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

[dead-claudia]

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

[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".

[the8472]

I don't think we can bolt on a termination checker onto Rust. That is use limited to proof assistants.

False negatives would be acceptable, just like in the borrow checker. Additionally the user could unsafely assert that a loop will terminate when rust can't determine that.

And while we're wishing for ponies in addition to total there are other desirable properties https://blog.yoshuawuyts.com/extending-rusts-effect-system/#what-are-effects

[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.