Hacker News Reader

Compilers and compiler writers don't rely on informal reasoning when deciding whether an optimization is valid

This can be modelled formally: just drop the ex falso quodlibet axiom and its equivalents.