Hello retard,
Tue, 01 Dec 2009 14:24:01 -0800, Walter Bright wrote:
dsimcha wrote:
My biggest gripe about static verification is that it can't help you
at all with high-level logic/algorithmic errors, only lower level
coding errors. Good unit tests (and good asserts), on the other
hand, are invaluable for finding and debugging high-level logic and
algorithmic errors.
Unit tests have their limitations as well. Unit tests cannot prove a
function is pure, for example.
Sure, unit tests can't prove that.
Both unit tests and static verification are needed.
But it doesn't lead to this conclusion. Static verification is
sometimes very expensive and real world business applications don't
need those guarantees that often. It's ok if a web site or game
crashes every now and then. If I need serious static verification, I
would use tools like Coq, not D..
Static verification in Coq is very expensive, but who really does that for
real world programs. I think we are talking about automatic static verification
with none or minimal programmer assistance - it will get you assurances for
larger project with multiple programmers - that various parts plug in correctly
(typecheck) and that they do not affect other parts of program in unexpected
ways (const/pure/safe) - then you are at good ground to verify yours program
logic by yourself (debugging/pre(post)conditions/unittests/asserts/invariants).
