4 ms·

As a small data point I'd say that Leslie Lamport claims that Amazon has used TLA+ on a good number of big projects; many people think of formal proving as an a

As a small data point I'd say that Leslie Lamport claims that Amazon has used TLA+ on a good number of big projects; many people think of formal proving as an activity that is separately layered on top of programming, as opposed to a proving-language. Also, when people use Rust, are they using proving techniques?

steveklabnik 8y ago
Not yet; we’re still working on the semantics of the language, and proofs for it; you need that before you can prove things about the code in the language. Or at least, the stuff we’re most interested in. The EU is funding some of this work.
- timClicks 8y ago
  For people interested in looking deeper, this work is called RustBelt. Useful web pages are the project's homepage (https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/) and the research paper describing the project (https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflayout=flat https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflay...)
snaky 8y ago
If you are interesting in a programming language suitable for system level programming, and using proving techniques, maybe ATS would be of interest. https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html