I'm always surprised by how thoroughly uninterested the Haskell and Rust communities are in learning from the Ada/High Integrity Software community.
Here you have people who are actually doing what you purport to be interested in (creating defect-free code) who have a great deal of experience and a great many insights from actually putting their code into avionics bays knowing that thousands of lives are depending upon it.
But they're not valley programmers. They skew older. Heck most of them don't even live in California. And they don't "get" what's so amazing about category theory as a programming paradigm so obviously they're morons. Plus they seem to be process-obsessed and that process ain't agile.
Maybe eventually the valley bros will rediscover most of what the Ada programmers already know.
Hm, I find this to be a pretty mischaracterizing view of Rust. Nobody on the core team lives in California. We never talk about category theory. Our average age is mid-30s. And in general, we love hearing about other languages, including Ada.
We're using Rust in building safety-critical runtime software for autonomous vehicles precisely because we do care about these kinds of things for non-R&D products.
We have many experiments showing how trivially easy it is to write MISRA compliant C, that normally passes muster for "safety-critical" in automotive, which is horribly unsafe, but for which analogous Rust fails to even compile.
We're also working to go many steps beyond ISO 26262 in terms of process and process verification. To the point that we're going to attempt to have a formally verified development lifecycle in addition to as much of the software that comes out of it being formally verified as well.
We're not stopping at formal verification for the software or process either due to fairly glaring gaps/shortcomings in the methods available today.
If we are talking about the community of users, the experiences of Ada programmers are likely of no little help to someone working with Haskell. Ada is an imperative language with explicit declarations and mutation everywhere. Its mechanims to help out with safety basically have to do with managing side effects.
> 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|8 years ago
Here you have people who are actually doing what you purport to be interested in (creating defect-free code) who have a great deal of experience and a great many insights from actually putting their code into avionics bays knowing that thousands of lives are depending upon it.
But they're not valley programmers. They skew older. Heck most of them don't even live in California. And they don't "get" what's so amazing about category theory as a programming paradigm so obviously they're morons. Plus they seem to be process-obsessed and that process ain't agile.
Maybe eventually the valley bros will rediscover most of what the Ada programmers already know.
steveklabnik|8 years ago
im_down_w_otp|8 years ago
We have many experiments showing how trivially easy it is to write MISRA compliant C, that normally passes muster for "safety-critical" in automotive, which is horribly unsafe, but for which analogous Rust fails to even compile.
We're also working to go many steps beyond ISO 26262 in terms of process and process verification. To the point that we're going to attempt to have a formally verified development lifecycle in addition to as much of the software that comes out of it being formally verified as well.
We're not stopping at formal verification for the software or process either due to fairly glaring gaps/shortcomings in the methods available today.
kazinator|8 years ago
bsder|8 years ago
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.