Re: Intervention needed?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2019-04-01 17:13, Optikos wrote:

>  One clarifying question that I have is:  how would you “prove no Constraint_Error propagating”?  At run-time or at compile-time or at engineering-time using tools other than the compiler?

It must be the compiler. The programmer states contracts of the 
subprograms and if the contracts cannot be proven to hold that is a 
compile-time error.

The problem is, of course, specifying the mandatory strength of a proof 
AKA false negatives vs. false positives. If a fact cannot be proven true 
by one compiler that makes the program illegal even if another compiler 
could prove it.

E.g. in the current Ada the program

    function Foo return Integer is
    begin
       raise Data_Error;
    end Foo;

is illegal, though every compiler can prove its equivalence to the legal 
one:

    function Foo return Integer is
    begin
       raise Data_Error;
       return 0;
    end Foo;

One way out could be user provided axioms which the compiler is allowed 
to use when it fails to find a proof (with a warning of course):

    function Foo return Integer is
    begin
       raise Data_Error;
## I swear there is a return statement
    end Foo;

> If at compile-time or at engineering-time using tools other than the compiler, then that is the solution that ATS2 and ATS3 are pursuing, where ATS's type views are rough analogues of what you are calling exception contracts here.

Exception contracts are not related to types. But otherwise, yes, SPARK 
must be integrated into Ada.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de