3 ms·
> On the proof side, Rust's built in unit testing is great, and allows for quick validation of code (proofs). But I think you mean something different. Unit te
by Joool 9y ago
> On the proof side, Rust's built in unit testing is great, and allows for quick validation of code (proofs). But I think you mean something different.
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.
- heavenlyblue 9y agoAnd 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.