3 ms·

This .... This kind of approach could and should replace rust. That is, if the language developers are interested in commercial adoption a sweet spot is a memor

This .... This kind of approach could and should replace rust. That is, if the language developers are interested in commercial adoption a sweet spot is a memory safer c++. Rust has that going on but it'll never make it as a truly safe language in memory and other aspects without specification and verification. I'm arguing real progress may include rust like impulses but can't be complete without built in tla+ or other formal tool support

dwohnitmok 6y ago
TLA+ operates at a different level both conceptually and in the SDLC than programming languages like Dafny or Rust. TLA+ is a design language rather than an implementation language and this permeates a lot of its foundations. FWIW you can already use Dafny to write individual modules in real-world programs (it compiles to .NET and therefore interoperates with e.g. C#), although there are still some rough edges given the tiny size of its community, and the documentation for doing this is rather fragmentary. As for the difference between Dafny and Rust, Rust really has only one big unique trick up its sleeve which is its affine types. Otherwise its approach is entirely compatible with Dafny's (and indeed there are efforts to port over some the same ideas between Dafny to Rust, see e.g. https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/). Those will take a long time though to come to fruition because formal verification is still a hard problem.
MaxBarraclough 6y ago
It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternative to C, not a more approachable formally verifiable language. That said, it looks like the good ideas from Rust may find their way into SPARK, a highly restrictive programming language for critical systems development with formal verification. [0][1] [0] https://www.adacore.com/papers/safe-dynamic-memory-management-in-ada-and-spark https://www.adacore.com/papers/safe-dynamic-memory-managemen... [1] https://arxiv.org/abs/1805.05576 https://arxiv.org/abs/1805.05576
- 1tCKV3QfIo 6y ago
  Go ahead, claim it's a safer alternative. It still suffers from many of the same problems that plague C. https://arxiv.org/abs/2003.03296 https://arxiv.org/abs/2003.03296
zozbot234 6y ago
> This kind of approach could and should replace rust. Rust could definitely be augmented with formal verification; it's just that this requires more research into semantics for Rust itself and Rust-like languages - especially wrt. the 'unsafe' subset.
chriswarbo 6y ago
If you're interested in a C/Rust-level language which supports verification, maybe take a look at ATS http://www.ats-lang.org http://www.ats-lang.org

dwohnitmok 6y ago

TLA+ operates at a different level both conceptually and in the SDLC than programming languages like Dafny or Rust. TLA+ is a design language rather than an implementation language and this permeates a lot of its foundations. FWIW you can already use Dafny to write individual modules in real-world programs (it compiles to .NET and therefore interoperates with e.g. C#), although there are still some rough edges given the tiny size of its community, and the documentation for doing this is rather fragmentary. As for the difference between Dafny and Rust, Rust really has only one big unique trick up its sleeve which is its affine types. Otherwise its approach is entirely compatible with Dafny's (and indeed there are efforts to port over some the same ideas between Dafny to Rust, see e.g. https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/). Those will take a long time though to come to fruition because formal verification is still a hard problem.

MaxBarraclough 6y ago

It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternative to C, not a more approachable formally verifiable language. That said, it looks like the good ideas from Rust may find their way into SPARK, a highly restrictive programming language for critical systems development with formal verification. [0][1] [0] https://www.adacore.com/papers/safe-dynamic-memory-management-in-ada-and-spark https://www.adacore.com/papers/safe-dynamic-memory-managemen... [1] https://arxiv.org/abs/1805.05576 https://arxiv.org/abs/1805.05576

1tCKV3QfIo 6y ago
Go ahead, claim it's a safer alternative. It still suffers from many of the same problems that plague C. https://arxiv.org/abs/2003.03296 https://arxiv.org/abs/2003.03296

zozbot234 6y ago

> This kind of approach could and should replace rust. Rust could definitely be augmented with formal verification; it's just that this requires more research into semantics for Rust itself and Rust-like languages - especially wrt. the 'unsafe' subset.

chriswarbo 6y ago

If you're interested in a C/Rust-level language which supports verification, maybe take a look at ATS http://www.ats-lang.org http://www.ats-lang.org