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.
> My current project chose SPARK due to its tooling and legacy applications in the high-integrity, high-assurance demands of the mission-critical sector.
Interesting! Can I ask what industry you're in? Aviation, military, medical...?
I've been involved in many sectors, but the current application is for show control software to operate stage lifts, performer flying rigs, scenic winches, car catapults, and on and on. Overhead hoisting and effects with people requires very high safety standards, and at the moment, most of this type of software is audited to decent safety standards, but not formally verified the way applications are in Ada/SPARK for the aerospace, railway, and military sectors. The tooling for SPARK has been tried and tested. I have been designing, building, installing, and maintaining specialized equipment for almost 30 years in the water, on land, in the air, and even in space.
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.
That work has happened and continues to happen as well, but in the meantime, this is still quite useful.