3 ms·

iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and sta

iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions. I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.

pjmlp 6y ago
Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842 https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-Applications/dp/0521197163 https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded Software Development for Safety-Critical Systems" https://www.amazon.com/Embedded-Software-Development-Safety-Critical-Systems/dp/0367338858 https://www.amazon.com/Embedded-Software-Development-Safety-...