Re:Why is Rust difficult?
by heavenlyblue on Monday January 22, 2018 @08:33AM
(#16204177)
And for anything more or less complex and optimised (e.g. Egalitarian Paxos), you'll not only end up with proving the correctness of the algorithm, but also the correctness of the implementation (which by themselves will hugely vary).
I see way more future in one's ability to write proofs of correctness in the comments before the function definition in any language; rather than preferring any specific language for the sake of proof.
Unit testing can only proof one instance of the input domain, e.g. the function square() returns 4 under the input 2. Languages like Coq allow you to proof that the function square returns the squared input for every possible input.