Re: What is wrong with Ada?

[Robert A Duff <bobduff@shell01.TheWorld.com>]

"Harald Korneliussen" <vintermann@gmail.com> writes:

> On Apr 12, 8:47 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>> There is no way to be sure the code is bug free!  Not in any language.
>> Not using testing, nor any other method (including so-called
>> proof of correctness).
>>
> In so-called dependently-typed languages, you can use the type system
> to ensure the correctness of a program, ...

OK, but if "correct" means "obeys a formal specification", then correct
programs can have bugs.  By "bug", I mean that reasonable users would
consider it wrong behavior.  In many cases, it's not even possible to
formally specify what's "right" or "wrong" behavior.  Proof: we've all
witnessed arguments where one person says "it's a bug", and the other
says "no, it's a feature".  ;-)

>...at least such a program as
> your primality checker. The type-theorists talk about this curry-
> howard isomorphism thing, which apparently is an isomorphism between
> programs and proof.
>
> I think the SPARK people would agree that there are indeed methods to
> assure that code is bug-free, at least to the extent that the
> specification is bug-free...

There's the rub.  I've read studies that claim about half of all bugs
are bugs in the specification.  And of course many programs have no
specification other than the program itself.

Note also that SPARK is a very simple language, intended for very simple
applications (i.e. safety is more important than fancy features).  If
you try to write, say, a windows operating system, or an Ada compiler,
in SPARK, I think you would have trouble.  That's fine -- it's not what
SPARK is for.

>... (and even that can to some degree be checked
> mechanically!). Not to say that it is easy, cheap, or even feasible in
> very many cases, but don't you underestimate a good type system.

Agreed.  SofCheck is makes a tool that can go far in this direction,
in a practical way.  But it's a dangerous mistake to think that
some method or other can completely eliminate bugs.

- Bob