3 ms·

Only if you are that exceedingly queer kind of programmer who thinks that which is not within reach of Coq can never be truth. I am a programmer, but I like C

• irishsultan 9y ago
  Well, you probably meant assert(A || !A), but even so that will of course never be an issue if A is a value, it becomes only a problem if A is replaced by something like a() (which I assume to be a pure function for the purpose of this comment). Of course a() || !a() is never going to be false either, so assert(a() || !a()) will never abort your program, but that doesn't mean a() || !a() will ever be true (if a() never finishes calculating then neither will a() || !a()).
• danharaj 9y ago
  (A && !A) is always false even if (A || !A) isn't justified . In other words, !!(A || !A). When we reject excluded middle we are no longer talking about truth, but evidence.