12 May
2005
12 May
'05
2:28 p.m.
On 5/12/05, Antonio Carlini <a.carlini at ntlworld.com> wrote:
John Hogerhuis wrote:
Yeah there can be no algorithm to test algorithm correctness. Halting
problem... so naturally you would have to restrict yourself to
something less than a turing machine to get this.
All computer scientists have ever proved is that
you could get
by without goto. They jumped to an unwarranted conclusion when
they decided it should never be used.
One of Dijkstra's interests was formal specification and verification:
basically unambigously describing what you want to do and then proving
afterwards that you've done it. You'll notice that the bit in the
middle doesn't get a look in :-) In fact, you could argue that the
bit in the middle needs to be constrained just so the proof is a
practical proposition.
So it's nothing to do with stifling your
creativity: be as
creative as you like. It's just unlikely that any of us
(including you) will ever know whether your prorams (or at
least any of them of significant size) are correct or not.
Agreed, but nor should anyone really care about provable correctness,
right? Engineering is about making things that are practically useful,
i.e. "good enough"-- we're not designing stained glass windows for the
Church of Reason, we're simply making and maintaining tools to solve
todays problems more efficiently than if those tools were not
available.
-- John.