Compilers

[peter.amey at praxis-his.com (Peter Amey)]

[snip]

> Isn't the whole basis of Spark a matter of adding proof 
> statements in the comments ?  I don't think the general 
> compiler marketplace would go for that built-in to compilers. 
>  After all:
>
>       1. The Praxis implementation can be used with multiple compilers
>
>       2. The compiler market is so immature that some people are still
>          using C, C++ and Java.
>
> But for the high-integrity market, Spark seems to fit the bill.
> --
> Larry Kilgallen

We think so!  However, like everything else, it is how you use things
that matter most.  What SPARK allows is very effective secure coding
(what this list is all about).  There is an entry on this subject on the
Build Security In website:
https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/sdlc/61
3.html.

regards

Peter