> Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer.
By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.
By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.