Hacker News Reader

Comment by codefined | Hacker News Reader

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?

View on HN

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 :)

> 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...

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.

Reply on news.ycombinator.com