> If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're veri

> If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're verifying the compiler from one language to the other. The specifications of the two languages are not that hard to implement. The difficulty is covering all cases in compiling from one to the other. The formal proof does tell us that we haven't missed any.