Masten Space Systems is using Ada and Spark to land on the Moon's south pole [pdf]

'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark?

'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations.

Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors.

Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada").

'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.

Not every domain affords you the luxury of coding the wrong thing and then fixing it in a later iteration. Sometimes due to financial constraints, other times because people wouldn't exactly be okay with the 0.7.1 version of your plane software leading to crashes until the next patch.

That said, i somewhat agree with you that UML and abstractions can only lead to problems if there's too many of them. A few high level overview diagrams can be good to have, but only as long as they conform to the actual architecture and models 1:1, and as long as they're not made at the expense of actually writing working software and perfecting it.

However, as long as only one person with incomplete knowledge of the domain or requirements is the one to write the code, you'll still end up with sub par solution. Personally, i think that the only way around that would be a paradigm shift of sorts - instead of planning meetings that aren't good enough, you might as well do programming meetings and mob programming in which you'd code the most important architectural bits of the software that you need, leaving the legwork for individual contributors later.

In my experience, code review is far too late for serious decisions to be made. At best, the reviewer will need to wrangle with hammering your sub optimal code into shape, at worst they'll just be like: "Sure, this looks like Java, it can go into the main branch. QA can figure out whether it's good enough or not."

This actually happened on Apollo 11. The 1201 and 1202 program alarms were the computer overloading, and running out of space for more processes. When this happened, the computer would reset, and navigation would pick up again.

Erlang didn't invent much there, and restarting/rebooting isn't always possible (try doing that in less than 10ms). Sometimes, the application itself needs to handle problems. This puts lots of 'classic IT' (interface bonding, fail overs, etc.) stuff to the bin very quick.

So every time you get that input you’ll still crash, but other transactions will continue normally. Hopefully that input is either due to a transitory glitch like a bit flipped in RAM, or a user who isn’t bored enough to keep submitting it, but either way the process isolation means all your other jobs can continue.