bearophile wrote:
Walter:
Ada is a failed language.
I agree that as general purpose language Ada is probably a failed language.
But currently Ada is often the best language still if you have to write the
autopilot software for an aeroplane or something that requires software with
minimal bug counts.
I don't believe that has been objectively demonstrated. It's a claim.
Even if today Ada is sometimes the best language to write an autopilot,
tomorrow the situation may change. Microsoft keeps developing its Sing#
language, and two Microsoft researchers have released "Verve", a little
experimental operating system kernel that has a nucleus written in typed
assembly statically verified, and Spec# or Sing# code... So maybe in future
high integrity software systems will be written like this instead of Ada
(typed assembly is nicer than the normal inline D asm even when it's not
formally verified, just verified by the type system, more or less like C
code).
Despite what the marketing literature on Spec# says, and what you repeated from
that, I was able to show within minutes that its contract proving feature is so
limited as to be effectively useless. Spec# doesn't do your hobby horse security
features, either.
In other words, I think you should be careful reading feature lists and lists of
claims put out by marketing departments. Whether a language feature delivers on
its promises is only born out by years of experience in the field writing real
software with real programmers.
The only way you're going to actually find out what is causing problems in the
field is to talk a lot with experienced programmers and their managers, and
doing things like reading the bug lists on major projects and trying to figure
out why those problems happened.
I do have some experience with this, having worked at Boeing on flight critical
designs for airliners. There are a lot of lessons there applicable to software
development, and one lesson is that armchair gedanken experiments are no
substitute for field experience in how mechanics actually put things together,
what kinds of mistakes they are prone to making, etc.
