🚀 go-pugleaf

joshua@athertn.Atherton.COM (Flame Bait) writes:

|   "Proving your programs are correct" seems to mean different things
|   to different people:

|   One group thinks it means that your program does exactly what your
|   spec says it should.

   ...

|   The first sort of proof is obviously useless, the spec becomes the
|   program, and bugs in the spec become bugs in the program.  Also,
|   specifing most programs is impossible; and if you could, then you
|   could write a compiler for the specification language.

I've seen this kind of remark several times in this multi-group discussion.
*It just isn't true*. Just because you can write a specification for a program
doesn't mean you can write a compiler for the specification language which
generates code, let alone acceptably efficient code.

Suppose I specify an square root function "sqrt" by:

    abs( sqrt( x ) ** 2 - x ) < 0.01

[Er - I'm not a numerical analyst; this fixed bound of 0.01 looks very suspect
to me, and I suspect that it's not the right kind of specification. But this
is a different issue.]

I claim this is a good specification (modulo the [...]) of the behaviour of 
"sqrt". Now tell me how you're going to generate code for sqrt from it, and
convince me that the code will be efficient, and that you have a *general*
mechanism that will do this for examples further removed from the Opening Book
of moves in the Specification Game.

I'll also think that the remark "specifying most programs is impossible" is
wrong. "bloody difficult, especially after the fact" is the predicate that
springs to mind.

Regards,
Kers.
--

Regards, Kers.
"If anything anyone lacks, they'll find it all ready in stacks."