Erlang rocks (Re: Eppur si sugat)

[Chris Pressey]

On 30 May 2003 00:47:31 +0200
Tony Rogvall <tony@REDACTED> wrote:

> On Thu, 2003-05-29 at 23:59, Chris Pressey wrote:
> > On Thu, 29 May 2003 00:58:27 -0700 (PDT)
> > "Dr.Dr.Ruediger M.Flaig" <flaig@REDACTED> wrote:
> > 
> > it's called "the human mind" :)
> > 
> > Seriously, I think it's a lot more effective for the programmer to
> > prove their code to his/herself while writing it, than to prove it
> > mechanically after the fact.  In fact I think most (good)
> > programmers do this subconsciously, and testing is part of it, to
> > reassure themselves that they wrote what they meant to write.
> > 
> 
> I guess this is a flame, I wont go for it :-)
> 
> /Tony

Not at all, my good man!  Although perhaps I stated it less than
elegantly.

Took me a while, but I managed to find where I picked up the notion:
_Theories of Programming Languages_ by John C Reynolds (Cambridge
University Press, 1998), p. 54 (emphasis mine):

"This is not to say that every program merits formal proof.  Experience
with formal proof methods, however, also increases a programmer's
ability to detect flaws in informal arguments.  The inference rules
introduced in this chapter are fundamental laws about imperative
programming, in the same sense that the associative, commutative, and
distributative laws are fundamental laws about arithmetic.  When
mathematically literate people perform or check an elementary algebraic
manipulation, they rarely descend to the level of applying such laws
explicitly, but their knowledge of these laws, and their experience in
applying them, underly their ability to avoid and detect errors.  _A
similar knowledge and experience of program-proof systems can buttress
such an ability for programming_."

Further on, p. 71:

"As a second example, we will prove the total correctness of a program
that computes x^n in log n time.  In this case, we want to demonstrate
that _one does not have to prove programs after the fact, but that
program proof can go hand in hand with program construction_."

p. 72:

"At this point, we have an informal account of the first step in a
top-down program construction: _we know how to write the program if we
can write a while body B with certain properties_."

In other words: start with the specification, derive the program from it
while proving it, and the program will be correct "out of the box".

Of course, running the program through a proof-checker after all is said
and done can't hurt either.  But it seems like the long way around, and
might be subject to the "seatbelt effect" where the programmer feels he
or she can afford to be sloppy, not realizing that mistakes, even when
caught, will still have to be fixed eventually.

To say nothing about determining whether the specification for a large
program is, itself, correct - oi!

-Chris