Super OT divergence because I am a loser nerd: On Thu, Jun 6, 2013 at 1:27 PM, rusi <rustompm...@gmail.com> wrote: > Yes, all programming communities have blind-spots. The Haskell > community's is that Haskell is safe and safe means that errors are > caught at compile-time.
I don't think Haskell people believe this with the thoroughness you describe. There are certainly haskell programmers that are aware of basic theory of computation. > Unfortunately* the halting problem stands. When generalized to Rice > theorem it says that only trivial properties of programs are > algorithmically decidable: > http://mathworld.wolfram.com/RicesTheorem.html > > And so the semantic correctness of a program -- a non-trivial property > -- is not decidable. Just because a problem is NP-complete or undecidable, doesn't mean there aren't techniques that give the benefits you want (decidability, poly-time) for a related problem. Programmers often only or mostly care about that related problem, so it isn't the end of the line just when we hit this stumbling block. As far as undecidability goes, one possibility is to accept a subset of desired programs. For example, restrict the language to not be turing complete, and there is no problem. Another resolution to the problem of undecidability is to accept a _superset_ of the collection you want. This permits some programs without the property we want, but it's often acceptable anyway. A third approach is to attach proofs, and only accept a program with an attached and correct proof of said property. This is a huge concept, vital to understanding complexity theory. It may be undecidable to find a proof, but once it is found, it is decidable to check the proof against the program. Haskell takes something akin to the second approach, and allows errors to exist which would require "too much work" to eliminate at compile time. (Although the type system is a literal case of the first resolution). Python, by contrast, often values flexibility over correctness, regardless of how easy it might be to check an error at compile time. The two languages have different philosophies, and that is something to respect. The reduction to Rice's theorem does not respect the trade-off that Haskell is making, it ignores it. It may be a "pipe dream" to get everything ever, but that's not to say that the entire approach is invalid and that we should ignore how Haskell informs the PL discourse. For some reason both the Python and Haskell communities feel the other is foolish and ignorant, dismissing their opinions as unimportant babbling. I wish that would stop. -- Devin -- http://mail.python.org/mailman/listinfo/python-list
