soundness
A -> B

A is my checker says something about the program

B is the program actually does that



while (0) {
}



completeness
B -> A