Hacker News Reader

Ada Spark goes beyond safety guarantees of Rust. However how many here want to prove their invariants hold for their UI?

View on HN

You 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.

How would you prove stuff about your code like memory safety.

Out 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

Reply on news.ycombinator.com