
Here here.
This reminds me of a recent discussion on the cafe. Thee OP amounted
to: What are the monad laws good for?. The answer was: It means the
monad doesn't do surprising things and its behavior is congruent with
the basic intuitions of sequenced computation.
In my eyes, proving nice properties about programs and moreover
calculating the programs themselves are pillars of computer science.
However, I think it's helpful (for this sort of presentation crafting)
to be aware of the disparity between computer science and most
programming in the trenches. That said, Sylvan points out that the
disparity isn't a unbridgeable schism--it's just that the concepts
don't yet map as directly as we'd like.
On 4/18/07, Sebastian Sylvan
On 4/18/07, Taillefer, Troy (EXP)
wrote: I have to strongly disagree with the statement that developers like to debug. Debugging is necessary because you can't reason about any "sizeable" piece of code just is not tractable even in Haskell. Now automated tools for reasoning about programs are very cool but lets face it no real world developer will sit down start to manually formally reason about large pieces of code.
I think the emphasis when mentioning "reasoning" really shouldn't be "you can reason formally about your programs and prove that they don't go wrong", nor "when it has gone wrong, you can reason about the program to figure out why", it should be "since the language doesn't do batshit insane things behind your back, your programs will mostly work the first time". The "reasoning" isn't an active task that you schedule time for, at least for a casual user like me, it's part of the actual programming. You do "reasoning" when writing in C++ as well, but you often get it wrong (because the language is, shall we say, unreasonable?) and that causes bugs.
-- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe