I have been teaching myself SPARK 2014 and there are a couple of article on writing different parts of drone software in SPARK. Rust also has my attention, but Spark goes beyond Rust’s current capabilities in proving a program. I started to look at F* and F# as a possible toolset, but SPARK has a lot of work behind it. It’s like the Python of the safe and secure programming world. I work on specialized machinery and rides, and we always perform a very formal HRA (Hazards Risk Analysis), and FMEA (Failure Modes and Effects Analysis), and I can’t believe nobody said what happens if the sensor fails!