I'll also add that perhaps a source of confusion is that assert(X) is presumed to take a bool at compile time. That is not the case, there are 3 outcomes: X==true : this has been proved to hold X==false: this has been proved to not hold X not computable: too weak theorem prover, check at runtime