5 ms·

The article makes a strong case. Even if rust allows formal verification, not all programmers use it, and if you use their library, you don't know if it's been

The article makes a strong case. Even if rust allows formal verification, not all programmers use it, and if you use their library, you don't know if it's been verified. Take it back to the goto analogy: can you formally verify goto? Yes. Does that mean it's good to include as a language primitive? No. You are basically taking an entire argument, ignoring its merits, and saying "but you can do it another way". You are exactly right, but you haven't rebutted the fact that structured concurrency is philosophically superior. I love rust and the community; they will get to the truth of this argument eventually. But I suspect the truth is that "njs was right", and I hope the it's sooner rather than later.

wilun 9y ago
It's not only that Rust allows formal verification, it's that it does it by default, writing unsafe Rust code for no serious reason is fundamentally frowned upon, and even then there is a serious effort to bring some tooling to bring more confidence even on "unsafe" Rust code. > But I suspect the truth is that "njs was right", and I hope the it's sooner rather than later. I'm not sure. The problem can and has been solved without the manually "pass the nursery object around" ""escape hatch"" for the general case of threads (because no: having the execution of spawning functions delayed by the lifetime of thread is arguably reasonable is some cases, but certainly not the general case of what threads are useful and used for) It is still useful for tons of existing languages as a pattern anyway, but only if the use cases are suitable. But the author is focused on a narrow use case of threads (and a narrow subset of the problems they introduce), and present their solution as a general truth and new fundamental control structure of computing, independent of already existing, in production, and arguably better solutions; and independent of analyzing the new problems their silver bullet introduces.
- iainmerrick 9y ago
  “Formal verification” for Rust code -- does that actually exist yet, or do people just hope/assume that the language will be proven consistent and that awesome theorem-checking tools will emerge eventually? I agree that Rust has a great model that seems to lead to very solid code, but “formal verification” is a high bar to clear.
  - wilun 9y ago
    Well, you are right, it is not really "formal verification". But I don't know how to call it, and it is way more checked on some aspects (well, obviously, we are not talking about checking each program against a spec...) that the competition. And by that, I mean that the competition is actually not even trying...
  - mikeurbach 9y ago
    Some people are actively working on formal verification for Rust. The RustBelt project is the first that jumps to mind. A paper and some discussion here: https://news.ycombinator.com/item?id=16302530 https://news.ycombinator.com/item?id=16302530
    - deleted 9y ago
      [deleted]
  - steveklabnik 9y ago
    We have a dedicated WG now actively working on it https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri...

wilun 9y ago

It's not only that Rust allows formal verification, it's that it does it by default, writing unsafe Rust code for no serious reason is fundamentally frowned upon, and even then there is a serious effort to bring some tooling to bring more confidence even on "unsafe" Rust code. > But I suspect the truth is that "njs was right", and I hope the it's sooner rather than later. I'm not sure. The problem can and has been solved without the manually "pass the nursery object around" ""escape hatch"" for the general case of threads (because no: having the execution of spawning functions delayed by the lifetime of thread is arguably reasonable is some cases, but certainly not the general case of what threads are useful and used for) It is still useful for tons of existing languages as a pattern anyway, but only if the use cases are suitable. But the author is focused on a narrow use case of threads (and a narrow subset of the problems they introduce), and present their solution as a general truth and new fundamental control structure of computing, independent of already existing, in production, and arguably better solutions; and independent of analyzing the new problems their silver bullet introduces.

iainmerrick 9y ago
“Formal verification” for Rust code -- does that actually exist yet, or do people just hope/assume that the language will be proven consistent and that awesome theorem-checking tools will emerge eventually? I agree that Rust has a great model that seems to lead to very solid code, but “formal verification” is a high bar to clear.
- wilun 9y ago
  Well, you are right, it is not really "formal verification". But I don't know how to call it, and it is way more checked on some aspects (well, obviously, we are not talking about checking each program against a spec...) that the competition. And by that, I mean that the competition is actually not even trying...
- mikeurbach 9y ago
  Some people are actively working on formal verification for Rust. The RustBelt project is the first that jumps to mind. A paper and some discussion here: https://news.ycombinator.com/item?id=16302530 https://news.ycombinator.com/item?id=16302530
  - deleted 9y ago
    [deleted]
- steveklabnik 9y ago
  We have a dedicated WG now actively working on it https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri...