3 ms·
Hm, so you write the code twice :)
by nullorempty 2y ago
Hm, so you write the code twice :)
- jpc0 2y agoYou make implicit assumptions you had during development explicit through code or comments which doesn't actually effect runtime execution speed since it only runs in debug/compile time. There's a place for formal verification, usually in places where a bug causes death or significant financial loss.
- PhilipRoman 2y agoYou're not wrong, but formal verification is still useful for multiple reasons: 1. Cases where specification is much less complex than implementation, like proving a sorting algorithm - the spec is very simple, forall integer i,j : i<j ==> result[i]<=result[j] plus the requirement that elements may not be removed or added 2. Ability to eliminate checks for improved performance (not sure if this applies to Rust yet, but it works great with Frama-C). 3. "Unit tests" for entire classes of behavior, not just specific inputs. Even if you cannot write a formal specification for a huge complex protocol, you can incrementally add asserts which cover much more area than simple unit tests.
- MaxBarraclough 2y agoIn a toy example like min/max functions, yes, the spec and the implementation look very similar. For more substantial problems that won't be the case, e.g. a sorting function.