Thanks but I only wanted to point out that there is a real dichotomy between an implementation and its proof of correctness, even up to isomorphism. But I mayb

Thanks but I only wanted to point out that there is a real dichotomy between an implementation and its proof of correctness, even up to isomorphism. But I maybe misunderstood what was being discussed!