> Do not write any code which you are not absolutely certain you could justify the behaviour of

Doing this for every line is impossibly tedious (people will quickly tire of it), and detecting where the code is actually non-trivial requires a kind of epistemic humility that doesn't come naturally to most.

Better if we can use languages that don't assume such demands are necessary for the compiler to be able to generate performant code.