> fret not, a second computer program can assure us of its validity Formal methods are rigorous enough and mature enough to be helpful in avionics software de

> fret not, a second computer program can assure us of its validity Formal methods are rigorous enough and mature enough to be helpful in avionics software development, why not in research mathematics? > I hope they are not building the foundations of future math on this house of cards. Mathematics is always a house of cards, and human mathematicians will always be fallible. It's already possible for a published result to later turn out to be invalid, in turn invalidating papers that relied on it.