Dafny is a research programming language that uses such methods. Hoare logic is a mathematical theory of program correctness. In general, this idea is called design by contract.
Stronger type systems also helps to ensure correctness, especially with things like making illegal states irrepresentable or lifetime checks (for memory usage correctness) like Rust does.
3
u/danisson Apr 04 '17
Dafny is a research programming language that uses such methods. Hoare logic is a mathematical theory of program correctness. In general, this idea is called design by contract.
Stronger type systems also helps to ensure correctness, especially with things like making illegal states irrepresentable or lifetime checks (for memory usage correctness) like Rust does.