They specifically said "compiling only proves correctness for the code being compiled, and for the properties covered by the type system".