Why not include little proofs in the code when you can? Several programming languages and libraries support Design-by-Contract (https://en.wikipedia.org/wiki/D

Why not include little proofs in the code when you can? Several programming languages and libraries support Design-by-Contract (https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract) which lets you specify preconditions, postconditions, and invariants directly in your code. Those predicates can be checked in various ways (depending on how deeply Design-by-Contract is supported) to help you know that your code is working correctly. Ada supports Design-by-Contract as part of the language: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... SPARK extends Ada Design-by-Contract into full proofs: https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html Rust has the Contracts crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/ Other programming languages have various levels of support or libraries for Design-by-Contract: https://en.wikipedia.org/wiki/Design_by_contract#Language_support https://en.wikipedia.org/wiki/Design_by_contract#Language_su...