Building a Virtual Mars Rover with SPARK and Rust

We have taken our Ada Mars Rover demo, featuring a physical robot driven by formally verified SPARK software, to the next level by introducing a simulator that allows you to experience the Rover's capabilities virtually. This simulation, implemented in Rust, accurately models the Rover's movement in an obstacle-filled environment, all while being controlled by the original SPARK code. This project exemplifies the synergy between Ada and Rust, demonstrating how these technologies can be effectively combined to build reliable, safety-critical applications.