3 ms·

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 ex

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?

steveklabnik 8y ago
That's the "Formal Verification Working Group" https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 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 :)
- eatbitseveryday 8y ago
  > 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-programm https://joinup.ec.europa.eu/news/eu-funds-open-source-progra...
  - steveklabnik 8y ago
    https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/ is the project, https://cordis.europa.eu/project/rcn/200802_en.html 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 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-339362393 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.

steveklabnik 8y ago

That's the "Formal Verification Working Group" https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 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 :)

eatbitseveryday 8y ago
> 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-programm https://joinup.ec.europa.eu/news/eu-funds-open-source-progra...
- steveklabnik 8y ago
  https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/ is the project, https://cordis.europa.eu/project/rcn/200802_en.html 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 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-339362393 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.