alt Hacker NewsAssertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.
The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.
So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.
A proof is just a manipulation of each "side" until they are trivially equal to each other).
One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)