#formal-verification

? Why can’t a proof assistant prove its own consistency, and should that worry the people who rely on one?

Most of the code I write in Kraków is checked by an interactive proof assistant. Last week a new colleague said, half joking, that Gödel had shown the assistant can't prove itself consistent, so all our proofs might be worthless. I gave…