3 ms·
Ada Spark goes beyond safety guarantees of Rust. However how many here want to prove their invariants hold for their UI?
by Ygg2 2y ago
Ada Spark goes beyond safety guarantees of Rust. However how many here want to prove their invariants hold for their UI?
- synack 2y agoYou don’t have to verify your whole application, just set SPARK_Mode => Off where you want to skip it. Alternatively, set the global default to Off and it becomes an opt-in feature. Proof levels depend on your goals, but most requirements are satisfied by proof of “Absence of Runtime Exceptions” (AoRTE), which is easier than a full formal proof.
- Ygg2 2y agoHow would you prove stuff about your code like memory safety.
- deleted 2y ago[deleted]
- synack 2y agoOut of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well. You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html https://docs.adacore.com/spark2014-docs/html/ug/index.html