Re:Announcing Rust 1.26.2
by codefined on Tuesday June 05, 2018 @03:42PM
(#17241322)
I remember reading a few weeks ago on Hacker News about a team of people who were working to mathematically prove that some of these issues are impossible in existing programming constructs. I can't entirely remember whether it was a thing people wanted to do or a thing that people were already doing, would you happen to know?
[ Parent
| on HN ]
Re:Announcing Rust 1.26.2
by steveklabnik on Tuesday June 05, 2018 @03:49PM
(#17241387)
That's the "Formal Verification Working Group" https://internals.rust-lang.org/t/announcing-the-formal-veri...
Participants range from "I'm interested in formal methods" to "my company uses formal methods and we're starting to apply them to Rust" to "The EU has given almost two million Euro for a university grant to prove Rust code" and everywhere in between :)
Re:Announcing Rust 1.26.2
by eatbitseveryday on Tuesday June 05, 2018 @04:59PM
(#17241990)
> Participants range from "I'm interested in formal methods" to "my company uses formal methods and we're starting to apply them to Rust" to "The EU has given almost two million Euro for a university grant to prove Rust code" and everywhere in between :)
Steve - can you give me a source for the latter? I'd like to read more into that, specifically.
edit: this? https://joinup.ec.europa.eu/news/eu-funds-open-source-progra...
Re:Announcing Rust 1.26.2
by steveklabnik on Tuesday June 05, 2018 @05:05PM
(#17242052)
https://plv.mpi-sws.org/rustbelt/ is the project, https://cordis.europa.eu/project/rcn/200802_en.html is the citation for the currency figure.
It's already borne some wonderful fruit. See https://www.ralfj.de/blog/2017/06/09/mutexguard-sync.html for an area where we were unsound, and https://github.com/rust-lang/rust/pull/45267#issuecomment-33... for an area where we were overly restrictive, and could remove some bounds without affecting soundness.