Re: Adacore joins with Ferrous Systems to support Rust

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

"Randy Brukardt" <randy@rrsoftware.com> writes:
> In any language with dynamic checks, one can easily reduce the problem
> of correctness down to simply proving that no check fails.

Well sure, but I'd take issue with the word "easily" there.  The
invariants for the red-black tree are fairly complicated.  Enforcing
them could be done with what I think SPARK calls a "ghost function" or
something like that: a piece of code that is not actually executed, but
is used only by the prover.  But, what would the proof look like?  I
think it would likely involve some manual work with an external proof
assistant like ISABELLE.  That takes quite a bit of effort and knowledge
on the programmer's part.

On the other hand, the RB tree type declaration in that Haskell example
is very natural and appealing even in that old implementation, and using
newer GHC features that have appeared since then, it becomes even nicer.

> So the question is how one can accomplish that with the least
> complication for the actual programmer.

Indeed.