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

[Shark8 <onewingedshark@gmail.com>]

On Friday, April 20, 2018 at 6:10:06 PM UTC-6, Paul Rubin wrote:
> Shark8  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.

What I mean by both of these is there are other items in-play, in such a combined HW/SW environment, than mere "correctness". There are properties that are absolutely crucial to specify and ensure: the Spectre and Meltdown bugs are examples of this (regarding the property of "access control" being violated because of the implementation of 'caching' and 'speculative execution' and interactions between them).

Proving properties is going to be one of the major things to allow for efficient parallelization, possibly chosen at runtime, to move things back to the realm of software. (The video https://www.infoq.com/presentations/Thinking-Parallel-Programming is an excellent progression into parallelism and culminates in just how important properties [algebraic in the talk, but generalizable] are.)

> 
> > 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.

That [proof in VHDL] would be good, too.
But having the compiler, the translator (VHDL-to-circuit), provable is necessary in order to ensure that the circuit you get *IS* the circuit described by the VHDL.

Full implementation conformance to H.3.2 (Pragma Inspection_Point) and H.3.1 (Pragma Reviewable) of Ada requires a lot of information; and H.3.1 (13) & (14) in particular thrust in the direction, though only requiring reporting, whereas this method is fully automatable and could produce exact, provable correspondence between source and object.

> 
> > 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?

How is it not?
Just because "best practices" of "the industry" says it's a-ok to have to clean and rebuild because the previous output was corrupted [perhaps a bad build-system] somehow doesn't mean it's not critical.

You have to keep rebuilding until it's *RIGHT*. (It's not hard real-time; but what happens to your SW company [I'll assume a SW-dev company because this is C.L.A.] if you never have any runnable executable? It'll die because it's not producing SW.)

But even disregarding hypotheticals, how important is it that your tools give you the right answer? [Often, very.]
Now, how important is it that the computer CPU be accurate [within its digital constraints]? (Intel FP error)
How about that your computer HW be correct? (Meltdown, Spectre; Phenom's TLB; Pentium F00F)

What we're talking about here is a system that produces both the software and the hardware; and so in order to have any assurance that you-as-a-programmer are getting what you specify (either HW or SW) as the output [if there is any output] the system-as-a-whole should be reliable. -- And, transitively, the criticality of software and hardware that would produced is part of the criticality of the compiler.

There are too many variables, too many outputs and possible inputs to make such an endeavor viable with testing methodologies -- it simply doesn't scale -- the only way that does scale is proof: the ability to say "here are the properties that must hold", feed the program to your provers, and verify that they do.

If we do the above with our compiler, then we have the excellent property that any modification we make to the IDE (and compiler(s)) retain the properties we proved and retain their correctness and, therefore, produce correct output.

And, after producing this verified compiler, we can have full confidence in what we compile with it is indeed what was specified -- for everything, regardless of its own criticality. 

> 
> 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.

Or you're left with a incorrect object. (I've had this happen, w/o an error message; then it dissapears when you clean/rebuild.)

But see above about the transitivity of criticality.

> 
> 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),

Those things are part of the variance of life and there's nothing we can do to eliminate them [esp. in the realm of SW], but we can [and do] mitigate them... like UPS in the case of power outage.

> 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).

Errors are fine, your compiler saying "Hey, I can only handle 128 parenthesis nestings" or "I can't represent 2**65" or "Hey, quit feeding me crap!" -- not that hose would be the actual error-text.

But that's qualitatively different than being able to say: this code that is output is provably correct in translation from the input.

> 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.

Every possible program WITHIN THE LIMITATIONS OF THE COMPUTER *AND* provably correct translation.

The key is in the intermediate representation -- you have the representation only able to represent syntactically (and, also, ideally) semantically correct Ada programs... Then you just need to prove production of the IR. (Let's assume that tokenizing is proved in a state-machine consuming characters or whatever.)

Lastly, you prove the code-generation of IR-to-target.

Done.

> 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)?

(1) I reject the idea that /CRASHING/ is at all in the same category as a controlled exit. You know the GNAT bug box? _THAT_ is a crash, you *don't* get the [should-be] actual error message from that.

(2) Why should there be a VC for maximum memory?

(3) Depending on the design, we could reduce a lot of memory usage. [There's a reason multiple passes were used in early resource-constrained machines.]

(4) But maybe it would be good to have an upperbound for what the compiler proper could use. [As opposed to, say, the IDE's own implementation of provers; which I imagine would only need correctness proof.]

> If there's not such a VC, how can you guarantee that
> your compiler never crashes from memory exhaustion?

Why are you so hung up on memory exhaustion?


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

Perhaps so; but the state of the industry is shameful. I mean look at how the filesystem is used as an ad hoc database in programming, or build-systems. Or the monstrosities called Continuous Integration [See the Experimental-DB/Workspaces paper upthread].

I believe there needs to be a bigger push towards correctness, and Ada probably needs a couple of good "killer apps" to really "cross the chasm", and a proven compiler/IDE would hit the mark on both of those.