Re: Adacore joins with Ferrous Systems to support Rust

["Randy Brukardt" <randy@rrsoftware.com>]

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87v8xwy3y7.fsf@nightsong.com...
...
> Well are you familiar with red-black trees?  They are a data structure
> similar to B-trees which you may have seen.  Basically the trees have
> nodes that are coloured either red or black, and there are some rules
> such as that internal red nodes can have only black children, and that
> enforces some invariants that keep the trees balanced so that lookups
> and updates are guaranteed to run fairly fast.
>
> Now these trees have been implemented in many languages, and if you look
> at almost any implementation, there is usually a test suite or internal
> debugging code to make sure that the invariants are preserved after
> doing an update.  It is quite easy to make a mistake after all.  But the
> Haskell code doesn't have those tests.  Why not?  Because the invariants
> are enforced by the datatype!  If you make a mistake and mess up an
> invariant, your code won't compile!  It's the difference between
> checking a subscript at runtime, and verifying that it in range with
> SPARK.  SPARK lets you get rid of the runtime check.  Haskell's type
> system is able to do similar things.

Cool, and most likely useless. OOP is like that in many ways, it lets you 
make a bunch of static checks, but to get them, you have to contort your 
design in awful ways. And then it is hard to extend, as you have a huge 
number of routines to override to get anything done.

I'm convinced that the answer (as much as there is an answer -- always 
beware of anyone bearing silver bullets ;-) is in the quality of tools (and 
language implementations). In any language with dynamic checks, one can 
easily reduce the problem of correctness down to simply proving that no 
check fails. So the question is how one can accomplish that with the least 
complication for the actual programmer.

Janus/Ada has a switch that can give you a warning for any implicit check 
that remains in the code after optimization. Combine that with the 
warnings-as-errors switch, and no program that could have a (detectable) bug 
can compile. Moreover, in Ada at least, one can introduce essentially any 
condition that you want to know as some form of assertion.

To take your red-black example. In Ada, I'd model the tree as a single type 
with two subtypes, with Red and Black predicates that enforce the 
conditions. Then, using the switches mentioned above, you could only compile 
the program if the compiler can eliminate the condition checks (it should be 
able to, if they are really complete).

The problem with this scheme, of course, is the quality of the 
implementation in terms of eliminating unneeded checks. For now, Janus/Ada 
can only do this sort of elimination inside of an extended basic block, and 
if something prevents a subprogram from being converted to a single extended 
basic block, you're likely to get spurious warnings. (And it only implements 
advanced elimination on a few kinds of checks, enough to prove the concept 
but not enough to be practical.)

The key for a programming language design is to minimize what Ada calls 
erroneous execution (undefined behavior), because it is that possibility 
which stop proofs in their tracks (or at least should; at least some tools 
ignore that possibility and essentially give garbage results as a 
consequence). Ada needs work in that area, but most other languages need 
more -- Ada at least detects most problems with dynamic checks.

Anyway, that's my 20 cents (inflation, you know). :-)

                             Randy.