Comments (6)
@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... 😅
from rfcs.
... detecting infinite loops.
there are two kinds of "non-totality" (expressions with type !
, excluding return
/break
/continue
)
- those that kills the execution:
panic!()
,abort()
,exit()
, infinite recursion (stack overflow) etc - 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".
from rfcs.
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
from rfcs.
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.
from rfcs.
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.
from rfcs.
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.
from rfcs.
Related Issues (20)
- Float rounding with specified digits HOT 4
- Refactor shared methods of `f32` and `f64` into new `Float` trait HOT 3
- Enable `Self = F` in generic `where` clause HOT 1
- Named opt-in trait impls HOT 2
- Question/proposal: Struct specialization HOT 3
- https://rust-lang.github.io/rfcs/0344-conventions-galore.html#lints uses `-` HOT 1
- new type of enum HOT 8
- Potential Compiler Optimization Issue with &Vec<Vec<T>> vs &[Vec<T>]? HOT 1
- Discussion/Pre-RFC/ACP: Unify privately constructed ("protected") ZSTs in std
- Create a struct similar to std::fs::File for directories HOT 2
- Converging let else HOT 1
- Conditional visibility: for integration testing purpose. HOT 1
- Enum of named structs boilerplate HOT 2
- [moved] Redefine `CARGO_TARGET_DIR` to be only an artifacts directory HOT 3
- Allow opting out of specific parts of core crate (e.g. core::fmt) HOT 11
- First-class compile time type manipulation HOT 4
- `move` `Copy` values HOT 5
- allow slice patterns to match non-fixed/generic length arrays HOT 6
- I built a tool for RFCs like Rust's
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from rfcs.