Open dead-claudia opened 1 month ago
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.
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.
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.
@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... 😅
... detecting infinite loops.
there are two kinds of "non-totality" (expressions with type !
, excluding return
/break
/continue
)
panic!()
, abort()
, exit()
, infinite recursion (stack overflow) etcloop {}
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".
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
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 inspirationdont_panic
built into the compiler.There's benefits to this that simply cannot be done in userland:
core::intrinsics::unreachable_unchecked()
, and then use this to check even debug builds for this. The usual linker approach simply cannot do this.#![no_std]
crates.My first thought is maybe a
total
keyword with the following rules:!
or a no-variant enum type are considered non-total except forcore::intrinsics::unreachable_unchecked()
!
or a no-variant enum type are considered non-totaltotal
modifier asserts the function is not possibly-non-total. Andtotal { ... }
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 toconst
.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.