12 May
2005
12 May
'05
6:45 p.m.
On 5/12/05, Antonio Carlini <a.carlini at ntlworld.com> wrote:
If we had a mechanism now to create provably correct
programs (that met specifications that we could be
sure meant what we intended them to mean) - and
further assuming that use of such a mechanism did
not impose excessive cost or efficiency burdens etc, -
then I think we would have to use them for all
serious programs.
That's a big if. I'm pretty well convinced it's a pipe dream. We'll
have reasoning machines capable of programming themselves when such a
scheme would prove useful (because I believe it is the same problem).
Of course if I had *this* I would use it (in fact, someone else would
be using it and I'd have to find a new line of work).
Today all you can do is trade a specification language for a
programming language. I think the programming language is the most
succinct, clear, and unambiguous specification language imaginable.
Almost always each construct has one and only one interpretation. You
cannot say anything in a programming language that cannot be done.
This is more clear on a small language like C or Forth or assembler
than it is in something like Perl or even C++. But true nonetheless
for those languages as well.
-- John.