undefined | Better HN

0 pointsmratsim6y ago0 comments

I did mention TLA+ (first link) or what were you referring to?

0 comments

3 comments · 1 top-level

agentultra6y ago· 2 in thread

> And that's where model checking / formal verification is a tremendous help (or would be if it was easier to use)

I assumed that statement was implying that understanding this problem in Rust is easier than in TLA+ which I disagree with.

I think TLA+ can state the problem and demonstrate it more clearly.

Apologies if I misunderstood! Text. I agree with your comment overall as a formal methods nerd/evangelist. :)

mratsimOP6y ago

I was actually arguing that the Rust community should definitely look into formal methods, in particular TLA+ and Ada/Sparks.

The borrow-checher/free-of-data-races/fearless-concurrency taglines are only focused on memory bugs and unfortunately the community is still focused on memory bugs as well.

Thankfully, it didn't prevent the Tokio team that had to deal with concurrency bugs (beyond memory safety) to write a model checker for Rust code called Loom https://github.com/tokio-rs/loom.

Nethertheless this proves that Rust should grow beyond the fearless concurrency/borrow checker narrative because concurrency brings a lot of problems and memory/lifetimes are only part of the equation.

agentultra6y ago

100% agree. I didn't know about Loom but I have been impressed by the adoption of TLA+ in different parts of Rust development.

j / k navigate · click thread line to collapse