Hacker News new | ask | show | jobs
by wilun 2983 days 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.
1 comments
iainmerrick 2983 days 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.

link
steveklabnik 2983 days ago
We have a dedicated WG now actively working on it https://internals.rust-lang.org/t/announcing-the-formal-veri...
link
mikeurbach 2983 days 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
link
wilun 2983 days 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...

link