Re: The future of Spark . Spark 2014 : a wreckage

[vincent.diemunsch@gmail.com]

Hello Randy,

> I think existing Spark is evil, in that it funnels off effort best applied 
> to the entire Ada language (or at least, a much larger subset). Computers 
> are now powerful enough that the excuses for avoiding proofs of exceptions, 
> dynamic memory allocation, and the like no longer are valid.

Spark imposes static memory allocation to be able to prove total correctness,
which means that the program will always do what is expected, which is required
by embedded softwares... 


> The Globals notation is much more important. We tried to design such a 
> notation for Ada 2012, but it became too much work to complete and there was 
> a lot of concern about getting it wrong. So we left this for the "experts". 
> It appears that the experts are working on it, which is good, because we 
> still want this capability in the next version of Ada (whenever that will 
> be). And for that to be the case, we'll need it to have proper Ada syntax 
> using aspects.

Ada has been designed so as to let global variables be freely accessed. Only a pragma was used to specify that a function is Pure (of side effects) and can be skipped for optimisation. Therefore it is now almost impossible to change that and that is probably the reason why you had so much difficulties to define the global annotation, which is trivial, because how will you deal with a procedure that have no annotation, but still uses global variables ? A simple warning at compile time ? Refuse to compile ?

Aspects syntax is ugly. It is simply the return of a kind of primitive language like LISP, done with words and arrows. It shows clearly that it is simply a workaround.


> No, to allow *compile-time* analysis of pre and post conditions. An Ada 
> compiler cannot look into the body of a package to see what is there, and 
> without expression functions, almost no compile-time analysis could be 
> accomplished. (We also need globals annotations for similar reasons.) The 
> real end-game here ought to be compile-time proof (that is, proofs that are 
> created as part of the normal compilation of Ada code).

A proof can't be generated at compile time ! The proof must be written independently, based on formal specification, and checked by an analyser, that may or may not be the compiler.


> Proofs of any kind should never, ever depend on anything in the package body 

As others told you, a proof is a proof that the implementation respects the specification, therefore it needs to make an interpretation of the package body.

> Spark users are on a certain dead-end, IMHO. The future is getting proof 
> into the hands of all programmers, as a normal part of their day-to-day 
>  programming. That requires that proofs aren't necessarily complete, that 
> hey use whatever information is available, and most of all, that they only 
> depend on the specifications of packages (never, ever, on the contents of a 
>  body).

But you seem to make also the confusion between a test and a proof, and that is exactly what AdaCore is doing now : they simply write the tests as post-
conditions and uses symbolic interpretation during compile time. I think that is what you mention by "into the hands of all programmers", ie even those with very few theoretical background.

It's a nice feature to sell and great fun for compiler writers but it's far from a mathematical proof and what Spark was able to do. But mathematical proof requires formal specification and that is far from the "all programmers" knowledge. The problem is that recent books on Spark completly forgot to speak of the necessary formal specifications (like Z for instance).


To conclude here is my vision of Spark and Ada :
- use Ada for things that are necessary for the compiler to produce the code and to express the semantic of the program.
- use Pragmas only as compiler directives, for specific implementation or optimisation (InLine, Ravenscar, Remote-Call-Interface...). Not for assertion, tests or whatever.
- everything that is related to formal verification should stay as comment in
the code. These comments can then be verified by external tools. There can be different levels of verification, not only the Spark vision.
- formal specifications are necessary for formal verification, therefore Spark should be able to make the link between formal annotations and formal specification.
- tests can be put either as comments or as external files, but please not as aspects. It is ugly to write the detail of a procedure in the spec.


Forget Aspects and worst expression functions : they are simply an error.
Mixing testing, specification and proofs as pragma or aspects or a combination of both of them will result in a too complicated language lacking of abstraction and a proper syntax.

Regards 

Vincent