[discreteevent]

A lot of certified safe systems are written in C++. I mean the ones that control the machine that could kill you. Response time is often a critical factor in safe systems. Also languages aren't as important as we would like then to be. Proof isn't used much for example because proofs are too difficult to review. Other techniques are more important like review, redundancy and testing. Safe systems tend to be more about boring old software engineering than computer science.

[lambdaelite]

I agree, the choice of programming language is one of the less important parts of the SDLC. In the case of Rust for SC work, as the linked article alludes to, what doesn't make sense to me is that there is no industrial-grade tooling or support software. It seems like an ill-informed statement.

As to proofs, I thought some level of formal proof was required at SIL4?