I believe that planes and trains are a success story of proof engineering—I only believe this anecdotally because proof engineers bring up planes and trains a lot when the topic of non-academic jobs comes up.
But crucially, I think Cinera is discussing a mathematical process of defining and understanding and communicating, where articulating the theorem in the first place or setting up lemmas for the proof can sometimes be “most” of the work. This process is, from a computer science perspective, “informal” because of how much human judgment and natural language is involved. So the question is less about formal verification than I think the direction you’re taking it is.
I believe that planes and trains are a success story of proof engineering—I only believe this anecdotally because proof engineers bring up planes and trains a lot when the topic of non-academic jobs comes up.
But crucially, I think Cinera is discussing a mathematical process of defining and understanding and communicating, where articulating the theorem in the first place or setting up lemmas for the proof can sometimes be “most” of the work. This process is, from a computer science perspective, “informal” because of how much human judgment and natural language is involved. So the question is less about formal verification than I think the direction you’re taking it is.
Geoffrey, you might enjoy my post from last year.