SPARK lets you write proofs - you can write different implementations of a function and prove at compile time they match some specification. An example of this

SPARK lets you write proofs - you can write different implementations of a function and prove at compile time they match some specification. An example of this is here: https://blog.adacore.com/gnatprove-tips-and-tricks-proving-the-ghost-common-denominator-gcd https://blog.adacore.com/gnatprove-tips-and-tricks-proving-t... Here's another post with some examples: https://blog.adacore.com/taking-on-a-challenge-in-spark https://blog.adacore.com/taking-on-a-challenge-in-spark There's a good book, Building High Integrity Applications in SPARK, that goes through things in detail. It's a good read for any programming language user to mine for ideas or explore how similar problems could be solved in their language: https://www.cambridge.org/core/books/building-high-integrity-applications-with-spark/F213D986a7D2E271F5FF3EDA765D48E95 https://www.cambridge.org/core/books/building-high-integrity...