Bools and explicitness [was Re: PyWart: The problem with "print"]

[rusi]

On Jun 6, 11:44 pm, Devin Jeanpierre <jeanpierr... at 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... at 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