4 ms·
But what point is there to an intellectual exercise if you don't know whether you've done it right in the end?
by hobin 14y ago
But what point is there to an intellectual exercise if you don't know whether you've done it right in the end?
- flatline3 14y agoThat's the point of the article. The claim is that he knows he has done it right because the declarative types are simple enough to understand as a whole, and they enforce and ensure correctness, verified through compilation.
- scott_s 14y agoUntil the code has actually been tested, he doesn't know that it works, he just thinks that it does. The above point is that he has not completed the exercise, by verifying what he thinks.
- flatline3 14y agoThe code was tested by the compiler, reducing the failure space to whether or not his declarative types are an adequate Proof. It's an amusing anecdote. Even when using Haskell, there are some obvious constraints to relying on the compiler as the sole validation of correctness.
- scott_s 14y agoThat's not good enough; you're still testing a proxy behavior, not the behavior under question. The hypothesis is, "Haskell's type system is robust enough that one can code an application through type checking alone." Doing the hypothesis is not testing the hypothesis; assuming the hypothesis is correct to demonstrate that the hypothesis is correct is begging the question. In particular, the kinds of errors that still may exist are ones where the implementer has a fundamental misunderstanding of what needs to happen. The code may correctly implement what he wanted it to do, but what he wanted it to do is wrong. If you still object, consider: I'm describing the scientific method.
- flatline3 14y agoI object because you're attempting to extrapolate an axiom from an anecdote merely intended to demonstrates the value and power of the type system.
- scott_s 14y agoMy point is we have not yet verified if the assumed conclusion of the anecdote is correct.
- wonderzombie 14y agoConsider that his Haskell program (ostensibly) relies on mathematical proofs, a chain of them. The compiler consumes and validates this chain of proofs and checks whether or not the program is "true." It's hard to imagine why you'd use the scientific method to verify that 1 + 1 + 1 == 3; basic math and logic--- something computers are good at--- are sufficient. As he and others have pointed out, the author was pretty up-front about the scale (relatively small; looks like a few hundred LOC) and nature (implementing an extant, well-defined API) of the problem. It's not an application as you suggest, and the author doesn't suggest it's a good idea for applications, either. The conclusion isn't "use Haskell & never test your code!". After all, he explicitly offers no conclusion. :) It's just an example of how, sometimes, you can be reasonably certain that your Haskell program is correct when it compiles. Myself, I'd still run it, or at least QuickCheck it. I don't trust myself not to write logically sound, completely incorrect code.
- yxhuvud 14y agoThe compiler can only test what he writes - not what he intends to accomplish.
- runeks 14y agoAh yes, the old question of "what is knowledge?".
- JadeNB 14y ago> Until the code has actually been tested, he doesn't know that it works, he just thinks that it does. After the code has been tested, he still doesn't know that it works, only that it sometimes produces the expected output. (As a mathematician, it's a lot easier for me to trust a proof than an empirical verification; but I agree that what the HM type system proves is not always what one wants it to prove.)
- scott_s 14y agoI agree. I claim that he knows that it works under the circumstance that he has tested, and can be more confident that it will work in circumstances similar to what he has tested.
- zopa 14y agoTrue. But with very general code, like this library, it would be difficult for unit tests to cover more than a small fraction of the domain.
- tikhonj 14y agoWell, unless he has a proof that the code works. I think the idea is that, in this case, the types are so polymorphic that they do constitute a proof.
- scott_s 14y agoThe insight behind Knuth's glib "I have only proved the program correct" quote is that proofs can still contain our untested assumptions. It's possible for someone to carry over an untested and wrong assumption from the implementation to the proof without ever finding out it is incorrect.
- tikhonj 14y agoOf course, the same is true for tests. If you prove the wrong thing, your code obviously won't be correct. If you test the wrong thing, your code obviously won't be correct. However, if you prove the right thing, your code is correct. If you test the right thing, you code is correct in the cases you tested. And yet, for whatever reason, only having tests is fine but only having proof isn't.
- scott_s 14y agoThere's no way to prove that you proved the right thing, unfortunately. And, of course, your proof may not be correct. (Proof checkers can help, and I would have confidence in the correctness of a type-check as proof.) Only having tests is "fine" for most circumstances because, unfortunately, proofs are intractable for most systems. During a software engineering talk I recently attended, an interview candidate stated that the largest proved-correct code base is on the order of 10,000 lines of code. Most people don't have the resources to do even that. But, philosophically, I always want tests for the same reason that I run experiments: I want empirical evidence, not just reasoning. Empirical evidence increases my confidence that we have accounted for what we think we have.
- srparish 14y ago"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Knuth
- hobin 14y agoTouché. I see your point.