It feels pretty clear to me that these Contracts should only be used for the “very certain” case. Writing code for a specific compiler flag seems very sketchy,

It feels pretty clear to me that these Contracts should only be used for the “very certain” case. Writing code for a specific compiler flag seems very sketchy, so the programmer should assume the harshest interpretation. The runtime check thing just sounds like a debugging feature.