I agree (with the caveat that I have much less relevant domain knowledge than Rohin, so you should presumably give less weight to my view).
Several years ago, I attended a small conference on ‘formal mathematics’, i.e. proof assistants, formal verification, and related issues. As far as I remember, all of the real-world applications mentioned there were of the type “catching bugs in your implementations of ideas”. For example, I remember someone saying they had verified software used in air traffic control. This does suggest formal verification can be useful in real-world safety applications. However, I’d guess (very speculative) that these kind of applications won’t benefit much from further research, and wouldn’t need to be done by someone with an understanding of EA—they seem relatively standard and easy to delegate, and at least in principle doable with current tools.
I agree (with the caveat that I have much less relevant domain knowledge than Rohin, so you should presumably give less weight to my view).
Several years ago, I attended a small conference on ‘formal mathematics’, i.e. proof assistants, formal verification, and related issues. As far as I remember, all of the real-world applications mentioned there were of the type “catching bugs in your implementations of ideas”. For example, I remember someone saying they had verified software used in air traffic control. This does suggest formal verification can be useful in real-world safety applications. However, I’d guess (very speculative) that these kind of applications won’t benefit much from further research, and wouldn’t need to be done by someone with an understanding of EA—they seem relatively standard and easy to delegate, and at least in principle doable with current tools.
Thanks Max—I’ll pass this on!