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

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

"Dan'l Miller" <optikos@verizon.net> writes:
> Coq is increasingly setting its sights on the wild-west worlds of C
> and machine code: [links]

Thanks, yes, I had seen some of those, will look at the others.  But,
it's a niche area.  Most programmers I meet these days have never
written anything in C or machine code.  Realtime programming in general
is a niche area: most programmers I know have never done any.  Critical
systems are also niche, and realtime critical systems are the most niche
of all.  And finally I don't know whether BIG critical realtime systems
exist at all; and if they do, whether they could be split up.

Ada, especially with high-end verification methods, is about the
intersection of it all, i.e. critical AND hard-realtime AND large.
Those are intense requirements and it takes a lot of work to satisfy
them.  If you aren't faced with those requirements, why do all that
work?  Non-realtime means you can use arbitrary precision arithmetic
(eliminating all those proofs about integer overflow) and garbage
collection (automating memory management).  Realtime but non-critical
means you can get adequate reliability from traditional software testing
instead of proof systems.  Realtime and critical, but not too large,
means you can jettison a lot of Ada's features and work with a much more
tractable subset (e.g. the original SPARK).

"Crossing the chasm" gives a picture of a large set of problems for
which Ada is the best solution, where the challenge is getting people to
appreciate this fact.  But I'm having trouble seeing the large set of
problems, especially once formal verification is part of the
prescription:

- If the problem is not realtime, it's probably easier to use a garbage
  collected language instead of Ada.  Realtime is a niche area of
  programming, so even if Ada completely takes it over, the "chasm"
  between Ada and the wider programming world is not even slightly
  crossed.

- If the problem is not critical (human safety is not endangered, and
  mistakes aren't enormously expensive to repair), then at least for
  now, verification is still much harder than ordinary testing.  If
  you're proposing making verification as easy as testing, that's great,
  but it's a mammoth research problem rather than a matter of
  straightforward advocacy or tool development.

- A lot of not-so-critical realtime code is being written in C (e.g. on
  embedded MCUs in consumer electronics).  I'd agree that we're probably
  better off if that stuff was instead done in Ada, with or without
  formal verification.

- Finally I think there are realtime problems like bit-banging comms
  protocols that might have been done with software back in the day, but
  that now get done with FPGA's (i.e. in VHDL or Verilog) now that
  FPGA's are cheap, since it's much easier to get deterministic timing
  with FPGA's than with CPUs.  So a fair number of applications have
  actually been removed from Ada's problem space.

> defines Ada's language semantics in English prose that compiler
> vendors cannot take as direct input into their compiler
> implementations.

Yes, this is an area where mechanized semantics would be a big win.
They had to do that for C in order to write CompCert.  You might look at
Twelf which is designed for such purposes.

> Speaking of SPARK, here is SPARK-esque analogue for a subset of C++:
> http://EscherTech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf

Thanks, this is interesting.