On Jun 6, 11:44 pm, Devin Jeanpierre <jeanpierr...@gmail.com> wrote: > > > 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. >
Nice 3-point summary. Could serve as a good antidote to some of the cargo-culting that goes on under Haskell. To make it very clear: In any science, when there are few people they probably understand the science. When the numbers explode, cargo-cult science happens. This does not change the fact that a few do still understand. Haskell is not exception. See below > > 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. Of course! Here's cmccann from Haskell weekly news of May 31: [On reimplementing cryptography in pure Haskell] writing in Haskell lets you use type safety to ensure that all the security holes you create are subtle instead of obvious. Which is showing as parody exactly what I am talking of: All errors cannot be removed algorithmically/mechanically. And here's Bob Harper -- father of SML -- pointing out well-known and less well-known safety problems with Haskell: http://existentialtype.wordpress.com/2012/08/14/haskell-is-exceptionally-unsafe/ ---------- > Super OT divergence because I am a loser nerd: Uh? Not sure I understand… OT: OK: How can you do programming if you dont understand it? I guess in a world where majority do it without understanding, someone who understands (more) will be called 'nerd'? > 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. Dunno whether you are addressing me specifically or python folks generally. If me, please remember my post ended with > If a programmer comes to python from Haskell, he will end up being a better > programmer than one > coming from C or Java or… If addressed generally, I heartily agree. My proposed course: https://moocfellowship.org/submissions/the-dance-of-functional-programming-languaging-with-haskell-and-python is in this direction. That is it attempts to create a new generation of programmers who will be able to use Haskell's theory-power to pack an extra punch into batteries-included python. More details: http://blog.languager.org/2013/05/dance-of-functional-programming.html -- http://mail.python.org/mailman/listinfo/python-list
