There is a paper online that proves fermat's last theorem in this way, by exploiting the C compiler's ability to optimize away non-terminating code that has no observable state changes.