3 ms·

I guess a bit of sarcasm but nevertheless. Excerpt from Kani doc : Kani is especially useful for verifying unsafe code in Rust. and regarding loom and shuttle

I guess a bit of sarcasm but nevertheless. Excerpt from Kani doc : Kani is especially useful for verifying unsafe code in Rust. and regarding loom and shuttle : Excerpt from The Rustonomicon : Safe Rust guarantees an absence of data races, which are defined as: 1) two or more threads concurrently accessing a location of memory 2) one or more of them is a write 3) one or more of them is unsynchronized However Rust does not prevent general race conditions. This is pretty fundamentally impossible, and probably honestly undesirable.

rurban 5y ago
concurrency safety does exist. checkout such languages, you'll be surprised. pony latest, but also singularity or concurrent pascal. also all other safeties rust only promises cannot provide
- newca12 5y ago
  Did you known that in its early days Rust did take a more Pony-like approach but as ownership/borrowing took shape it was obvious that it was more scalable to move that abstraction into libraries. What safe mean is not that easy to define. From the Pony FAQ: Pony prevents data races. It can’t stop you from writing race conditions into your program. Also keep in mind that Rust is not garbage collected, the guarantees Rust provide regarding safety are a huge step forward but of course a lot need to be done. Those guarantees are not promises, they are formally proven : https://www.ralfj.de/research/thesis.html https://www.ralfj.de/research/thesis.html (https://www.eurekalert.org/news-releases/610682 https://www.eurekalert.org/news-releases/610682)
  - rurban 5y ago
    safe is trivial to define. all the safe languages defined and implemented it. with rust we are still waiting for those promises. remember how eBPF was formally proven to be safe also? until meltdown came along and all those proofs fell down.
    - newca12 5y ago
      Ho well probem solved then. I wonder why people keep searching ;-)
    - kaba0 5y ago
      With all due respect, you don’t know too much about this topic to have such a strong opinion. There is no safe language, as that would imply the solution of Rice’s theorem, Halting problem, etc.

rurban 5y ago

concurrency safety does exist. checkout such languages, you'll be surprised. pony latest, but also singularity or concurrent pascal. also all other safeties rust only promises cannot provide

newca12 5y ago
Did you known that in its early days Rust did take a more Pony-like approach but as ownership/borrowing took shape it was obvious that it was more scalable to move that abstraction into libraries. What safe mean is not that easy to define. From the Pony FAQ: Pony prevents data races. It can’t stop you from writing race conditions into your program. Also keep in mind that Rust is not garbage collected, the guarantees Rust provide regarding safety are a huge step forward but of course a lot need to be done. Those guarantees are not promises, they are formally proven : https://www.ralfj.de/research/thesis.html https://www.ralfj.de/research/thesis.html (https://www.eurekalert.org/news-releases/610682 https://www.eurekalert.org/news-releases/610682)
- rurban 5y ago
  safe is trivial to define. all the safe languages defined and implemented it. with rust we are still waiting for those promises. remember how eBPF was formally proven to be safe also? until meltdown came along and all those proofs fell down.
  - newca12 5y ago
    Ho well probem solved then. I wonder why people keep searching ;-)
  - kaba0 5y ago
    With all due respect, you don’t know too much about this topic to have such a strong opinion. There is no safe language, as that would imply the solution of Rice’s theorem, Halting problem, etc.