[bsder]

> I'm always surprised by how thoroughly uninterested the Haskell and Rust communities are in learning from the Ada/High Integrity Software community.

If you read the paper you would find that the VAST majority of issues were human communication or understanding of the problem. No programming language can fix that.

Rust was started with one overriding goal: make programming on Firefox manageable. And they identified a primary problem: uncontrolled sharing. And they killed it: Rust disallows sharing by default. Everything else in Rust stems from that. "category theory" or any other academic CS is used when it helps the primary mission--otherwise it gets deferred.

> Maybe eventually the valley bros will rediscover most of what the Ada programmers already know.

And yet Ada exists practically nowhere that requires timely deliverables. Funny that.

Much like Lisp, if Ada were such a force multiplier, there would be someone who would use it to make lots of money.

[jordanb]

A few years ago, AdaCore's Robert Dewar observed that nobody has ever been killed by a flaw in Avonics software. That's perhaps not a good elevator pitch for a hockey stick startup but it's a good testament to the capabilities and skills of the people in the High Integrity community.

It's true that High Integrity development is not compatible with deadline or budget driven projects.

But there is a lot to learn from the High Integrity community and I think it's a shame that people who claim to be interested in making software more reliable ignore a community with decades of experience doing just that.

[bsder]

> A few years ago, AdaCore's Robert Dewar observed that nobody has ever been killed by a flaw in Avonics software.

While that may be technically correct, I would consider the crash of Air France Flight 447 to be partially an avionics software failure.

Responding to an inconsistent airspeed measurement by disconnecting the autopilot and then dropping into a weird, modal operating state (alternate law) and throwing control over to the very surprised humans counts as a software failure in my book. Having a stall warning that tells you to do the wrong thing is a software failure in my book (the stall warning turned off when inputs were invalid, but then turned back on when the pilots actually made the correct maneuvers because the inputs weren't invalid anymore).

While ultimately the failure for that flight was human error, a smart reaction by the software at any point would have prevented that tragedy. The biggest "smart reaction" would have been to flag the invalid airspeed to humans but don't change anything.

Whoever thought that dropping a suddenly dynamic system into the hands of surprised humans was a useful action should be shot. In reality, nobody thought it. Each individual subsystem had their own failure procedures, and nobody ever tested what happened when they interacted.

[Gibbon1]

> partially an avionics software failure... Responding to an inconsistent airspeed measurement by disconnecting the autopilot and then dropping into a weird, modal operating state

You could write that software in rust to do exactly the same thing.

[bsder]

Quoting myself upthread:

> If you read the paper you would find that the VAST majority of issues were human communication or understanding of the problem. No programming language can fix that.

At no point did I argue that Rust would have prevented the Air France Flight 447 kind of failure. However, neither would Ada have prevented this kind of failure.

I WAS however taking issue with the quoted "nobody has ever been killed by a flaw in Avonics software".

[Gibbon1]

> Avonics software

It's not the software that killed people it's the spec.

[im_down_w_otp]

Welcome to the entire basis of SAE Level-3 autonomy. Yes, it does often seem fairly silly.

[yjftsjthsd-h]

> And yet Ada exists practically nowhere that requires timely deliverables. Funny that.

Yes, the people who prioritize "working" over "correct" make sloppy mistakes and avoid the languages that would make them be less sloppy.

> if Ada were such a force multiplier, there would be someone who would use it to make lots of money.

The embedded world sends its regards.

[pjmlp]

Ada exists where killing people is not an option for sloppy programming.

The moment software companies start to actually pay heavy fines and are forced to do refunds for sloppy software like in other industries, the situation will change.

[Gibbon1]

Probably an advantage of Ada vs other languages, hard to find a sloppy Ada programmer.