4 ms·
As I said above, you can verify/prove the invariants you capture in the types. I don't know what you mean by "correctness of loops", but if you capture whatever
by pka 10y ago
As I said above, you can verify/prove the invariants you capture in the types. I don't know what you mean by "correctness of loops", but if you capture whatever it means in a particular type, yes you can.
If you really wanted, you could derive a proof that pi is equivalent to some sort of corecursive series, which you can then evaluate in a dependently typed language, I guess. A proof is a type.
On the other hand, how would you write a unit test that checks whether something calculates pi without comparing its result to pi itself?
- kazinator 10y agoIf I really wanted to waste my time, yes. > A proof is a type. Yes, Curry-Howard and all that. If I just write a well-typed function which supposedly calculates pi, the rather trivial well-typedness is not informative by itself. You're talking about adding reams of verbiage requiring expertise in using an advanced type system for executing a proof. This isn't how static type systems are actually used and advocated in the field, and it is not feasible in general, only for toy, academic examples. The proof code, which will exceed the size of the original function by at least an order of magnitude, could also be buggy. At the end of the day, it's just more code. It reminds me of the argument fropm the Lisp camp: "Well, I could just write (supermacro ...) which implements any syntax and semantics whatsoever". (No, in fact you can't, and the proof is that you never actually will.)