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

[Devin Jeanpierre]

Super OT divergence because I am a loser nerd:

On Thu, Jun 6, 2013 at 1:27 PM, rusi <rustompmody 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.

> 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