Nice interview. What a tremendous achievement to formally prove the correctness of a C compiler! It boggles my mind why more people are not involved in this direction.
I hope to live to see the day when lots of commercial software will be written with formal proofs and zero tests. It may just be that we don't have the right tools at this point. If theorem provers could figure out details for themselves for the most part and the programmer has to only specify a few key invariants and rough sketches of the hypotheses and the end guarantees then I cannot begin to imagine how much more productive programming can become.
I hope to live to see the day when lots of commercial software will be written with formal proofs and zero tests. It may just be that we don't have the right tools at this point. If theorem provers could figure out details for themselves for the most part and the programmer has to only specify a few key invariants and rough sketches of the hypotheses and the end guarantees then I cannot begin to imagine how much more productive programming can become.