[PRL] the "success" of types

[William D Clinger]

Matthias wrote:
> Mitch made fun of my challenge to the holy gospel of "types are a
> success story" at the beginning of Viktor's talk. While I considered
> discussing this with him privately, I think a "public" discussion will
> benefit everyone else more.

Sure.  Bring it on.

Mitch wrote:
> If you apply a little denotational semantics, every programming
> language is functional ;)

Yep.

Matthias wrote:
> That's of course bogus and not worthy of consideration. [It's almost as
> bad as discussing syntax.]

That kind of argument is worse than bogus.  It's just name-calling.

Mitch:
> But this has nothing to do with "functional programming."  It is very
> clear that Floyd, Hoare, Dijkstra et al thought about invariants as a
> way of managing the complexity of state in imperative programs.

Matthias:
> 2. So why has the checking of invariants been such a massive failure in
> imperative languages? Programmers have neither taken to writing down
> invariants; reasoning out their programs with wp, sp, wlp or other
> things; proving them correct with fancy pens etc.

First of all, checking of invariants is not at all the same thing
as thinking about them or writing them down.  Secondly, programmers
are often bad about writing down invariants in both imperative and
functional languages.  You could abbreviate that sentence to its first
five words.  Thirdly, good programmers do tend to write down invariants,
in imperative languages as well as in functional.

Mitch:
> Invariants (whether or not they are expressed through types) are
> important for both, and we shouldn't conflate the benefits of
> types/invariants with the benefits of functional programming.

Matthias:
> I can't follow the argument.

Which part don't you understand?  That invariants are important?
Or that we shouldn't conflate their benefits with the benefits
of functional programming?

Matthias, speaking of impure functional programming:
> 4. When this style of programming started leaping into mainstream
> languages (and will continue to move over), type checking there started
> to make sense.

Soon after Nixon resigned, type checking of imperative programs
started to make sense.  Java's superior type safety became a real
threat to C++ when Clinton was impeached.  If Dubya's approval
ratings continue to decline, we should expect further technical
improvements.

Will