Re: How to get Ada to “cross the chasm”?

[Paul Rubin <no.email@nospam.invalid>]

Shark8 <onewingedshark@gmail.com> writes:
>> Why do you say that?  Even for ordinary testing, not extraordinary?
> Meltdown and Spectre -- which stem from caching and speculative execution.

What does that have to do with anything?  

> It's about the *properties* here, not just whether "A:= 1 + A;"
> correctly generates an increment, or whether it can overflow.

I can't tell what you mean by this.  I may be missing something basic.

> In such an IDE the VHDL has to have some manner of proving properties;

That sounds like you're talking about proofs embedded in the VHDL code,
that prove SPARK-like VC's about the circuit being described.  That's
fine and necessary.  But the topic I asked about is the proofs used in
the compiler, not the proofs embedded in the compiled program.

> Never crashing is a good thing; it's far better to have a controlled
> exit than possibly leave things in a inconsistent state.

1. Of course it's a good thing, but is it CRITICAL?  For a jet engine it
is critical.  For a compiler I'm claiming it's not critical.  I'm open
to persuasion but at the moment I don't see the other side.  Let's put
it another way: you are running a crashfree compiler when a mischievous
billionaire offers you $10 million if you let him smash your computer
with a sledgehammer (setting you back a day or so while you buy a new
computer and restore your backups to it).  If you take the $10 million,
I claim you would have been ok without the crashfree compiler.

2. What inconsistent state is left if the compiler crashes?  It's just a
usermode program.  There's an error message saying that the compiler
crashed, and hopefully some diagnostic info saying how the crash
happened.

3. There are many ways compilation can fail, even if the compiler
software is perfect, such as a power failure in the office, problems
with the computer hardware, the building being hit by a meteor or
tsunami, or the above-described mischievous billionaire showing up.  At
a typical office there's maybe 1e-3 chance that one of those things
happens on a given day (the billionaire is the least likely of course),

With a well-tested compiler (verified like CompCert, but not SPARK
verified), you have at worst 1e-6 chance of hitting an input that it
can't compile (you get an error message instead, not wrong code).  How
much are you willing to pay to decrease the 1e-6 to 1e-10 by using
SPARK?  If the amount is more than zero, what are you doing about the
1e-3 chance of other problems?

Anyway, you have not explained how it's even conceptually possible to
write a SPARK verified Ada compiler that compiles every possible Ada
program, rather than a restricted subset.  If there's a VC requiring the
compiler to never use more than N bytes of memory, then what do you do
with an input that uses N+1 levels of nested parentheses (rejecting it
and printing an error message is no different than crashing and printing
an error message)?  If there's not such a VC, how can you guarantee that
your compiler never crashes from memory exhaustion?

Really, SPARK is great, but I think I'm seeing some overreaching claims
for it in this thread.