Is static typing really what you want? I would think that if you want safety against failure, you really want redundant systems that live in separate failure domains and can coordinate in the event of failure.

Why can't you have that with static typing? Btw I think only strong static typing really helps (C is statically typed but allows way too many implicit conversions).

There's also the question of what you regard as safety. Fault tolerance (like in elixir/erlang), or a design for fewer faults (e.g. ADA/Rust)?

Fault tolerance is good for high availability, which can be a safety goal (e.g. What does your airplane do when all the computers are off?) it doesn't help you however if yoir software didn't crash but does the wrong thing (like the boeing).

For the second part, strong static type systems definitely help, they provide clear documentation what can and can't be done, and they cause as many compile time errors if you do the wrong thing as possible. It doesn't rule everything out, but it gets you closer to the goal of correctness.

Fault tolerance is still needed. Usually you want to have redundancy (I think most airplanes use 5 controllers calculating at the same time to prevent atmospheric radiation causing bit flips to cause issues). And you want the system to go into safe states (e.g. Detect a fault and reinitialize, if that doesn't work do your best to stay operational until you've reached safety).

I think we could probably take over some of the supervision ideas from elixir, but combine it with strong static typing guarantees.

Static typing doesn't help you if your software doesn't crash but does the wrong thing (like the Boeing). In that case not even dimensional analysis helps you, because by my understanding that code was really stupid.

I find that if you're only documenting via types, that's a problem. You should also document by writing documentation.

I dont think anybody argues that types replace documentation. However, documentation without types tends to get repetitive and requires you to come up with ways to structure it properly. Turns out, you can encode a lot of information into a type and now it can be automatically verified and frees you to write documentation for things that can not be expressed in types.

Our safety critical languages need to be simpler, so they are amenable to mechanical proofs and exhaustive model checking. Dimensional units would be a good start.

https://gmpreussner.com/research/dimensional-analysis-in-pro...

F# has those built in (not mission critical embedded ready, but a very very nicely designed language).

ADA hat strongly typed fixed point built in. Rust I think has a strong enough type system to implement this as a library, at least there seem to be a few.

Idris also looks interesting. Maybe something like this can be done with dependent types.