A great first step in getting Rust in the high-integrity arena with the likes of Ada/SPARK. First, a specification, and then tooling to allow for formal verification ala SPARK. My current project chose SPARK due to its tooling and legacy applications in the high-integrity, high-assurance demands of the mission-critical sector. Hopefully, there will be a stable version to avoid having to update the Rust spec. too often. SPARK 2014 is the latest version, and it is based on Ada 2012. Stability leads to wider adoption for these types of applications. I also like the cross-pollination going on between Rust/Ada/SPARK.
I had expected to see a more programming language theory flavored formal specification, but it's actually just prose describing the language for industrial conformance purposes. I guess something is better than nothing, but still.
A great first step in getting Rust in the high-integrity arena with the likes of Ada/SPARK. First, a specification, and then tooling to allow for formal verification ala SPARK. My current project chose SPARK due to its tooling and legacy applications in the high-integrity, high-assurance demands of the mission-critical sector. Hopefully, there will be a stable version to avoid having to update the Rust spec. too often. SPARK 2014 is the latest version, and it is based on Ada 2012. Stability leads to wider adoption for these types of applications. I also like the cross-pollination going on between Rust/Ada/SPARK.