6 ms·
I highly doubt that you can prove correctness with types alone. How would you verify the correctness of this function with types alone: Integer add(Integer a,
by exi2 10y ago
I highly doubt that you can prove correctness with types alone.
How would you verify the correctness of this function with types alone:
Integer add(Integer a, Integer b) {
return a + b;
}
How would types verify for me that the result is correct and not a+b+1?
Formal proofs work for this but to make them work you need more than just types.
- omaranto 10y agoThe return type of your function is too broad: It should be the "type of integers which can be proven to be the sum of a and b". That sounds like a joke but it's what going overboard with dependently typed programming languages is like.