| 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. |
I find that if you're only documenting via types, that's a problem. You should also document by writing documentation.