Re: SPARK: What does it prove?

["Peter C. Chapin" <pcc482719@gmail.com>]

Rod Chapman wrote:

> Well..not quite.  The VC generator was constructed and very much
> based on the formal semantics for SPARK83 that was
> contstructed in the mid-1990s.  We have _lots_ of confidence
> that this semantics is completely upwards-compatible
> and consistent with the canonical semantics of Ada95 and
> this SPARK95 SPARK2005.

That's interesting to know. Thanks.

> There are also lots of assumptions tha underlie any
> "proof" of anything - in our case the integrity of the compiler,
> linker and the rest of the build environment...

Yes, definitely. This was a point I tried to make in a different thread
related to testing SPARK programs (and the value of doing so). SPARK helps
show that the source code is in some sense correct, which is great, but
that's not the whole story.

> In short: it seems to work.

Absolutely. I hope you didn't take my post as a criticism of SPARK. If the
goal is to reduce errors in actual deployed programs, which at the end of the
day is the important thing it seems, then I agree that SPARK works!

Peter