Re: How to get Ada to "cross the chasm"?

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

On 2018-04-26 19:38, Mehdi Saada wrote:
> Please bear with my ignorance, but from the exterior, it does seem that verification can switch on or off at a very fine level of granularity. At least in Spark 2014, with pragma spark_mode on/off.
> I'm surprised to read that seniors/experts like Randy almost despise Spark. Can you provide more information ?
> Do you find that:
> 1) the idea of proving formally is most of the time too much time consuming/almost not feasible for humans ?

It is impossible to prove everything, neither theoretically nor 
practically. Therefore the statement must be qualified - what is it you 
are going to prove.

> 2) good idea, but badly integrated with the language ?

It is an excellent idea. E.g. types conformance is proved because the 
language is statically typed and it is almost zero cost for the 
programmer. Other things may have low, medium, intolerably high cost or 
impossible. The language must allow to specify what exactly must be 
proved in the form of contract specification.

> 3) good idea, but the focus on it made designers lose focus on improving soundness of the language, so that the compiler would not need additional tools and efforts to achieve the same level of code quality ?

In my view they have been focused on wrong things all the time since Ada 
2005. E.g things like limited aggregates and return, dynamic predicates 
only diminish language soundness.

> I suspect it's 3. Are there elaborated critics of the formal proof tendency somewhere on the web, NOT coming from C or some lazy/poorly typed language's people ?

There is no point in that critique unless they object all-or-nothing 
approach, which is then a tautology, because that thing is nonexistent 
anyway.

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