I do some work on formal verification, so I can talk about it from that perspective. Purely functional code is the easiest to reason about, but then again you a

I do some work on formal verification, so I can talk about it from that perspective. Purely functional code is the easiest to reason about, but then again you a) can't interact with the "real world" in pure code, and b) "safety critical" often goes hand in hand with "embedded" and "low-level", where you usually don't want to lug a runtime around. So you will probably end up with an imperative language of some sort or the other. In such a case, the programming languages and programming practices which facilitate formal reasoning are more or less the same ones which facilitate informal reasoning. Avoid "spooky action at a distance", i.e. keep state changes localized (this enables you to use, say, separation logics). Funky flow control is difficult to model/reason about. Non-determinism as well. Type safety and static type systems help. Then again, if "safety" includes "security", you not only have to wonder whether your system is correctly implementing its API, but also whether the API is secure in itself. A paper by Steel & al [1] contains a partly amusing, and partly frightening account of one such investigation. [1]: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pd...