Chiming in on this very late. (I worked on formal verification research using proof assistants for a sizable part of undergrad.)
- Given the stakes, it seems like it could be important to verify 1. formally after the math proofs step. Math proofs are erroneous a non-trivial fraction of the time.
- While I agree that proof assistants right now are much slower than doing math proofs yourself, verification is a pretty immature field. I can imagine them becoming a lot better such that they do actually become better to use than doing math proofs yourself, and don’t think this would be the worst thing to invest in.
- I’m somewhat unsure about the extent to which we’ll be able to cleanly decompose 1. and 2. in the systems we design, though I haven’t thought about it much.
- A lot of the formal verification work on proof assistants seems to me like it’s also work that could apply to verifying learned specifications? E.g. I’m imagining that this process would be automated, and the automation used could look a lot like the parts of proof assistants that automate proofs.
Chiming in on this very late. (I worked on formal verification research using proof assistants for a sizable part of undergrad.)
- Given the stakes, it seems like it could be important to verify 1. formally after the math proofs step. Math proofs are erroneous a non-trivial fraction of the time.
- While I agree that proof assistants right now are much slower than doing math proofs yourself, verification is a pretty immature field. I can imagine them becoming a lot better such that they do actually become better to use than doing math proofs yourself, and don’t think this would be the worst thing to invest in.
- I’m somewhat unsure about the extent to which we’ll be able to cleanly decompose 1. and 2. in the systems we design, though I haven’t thought about it much.
- A lot of the formal verification work on proof assistants seems to me like it’s also work that could apply to verifying learned specifications? E.g. I’m imagining that this process would be automated, and the automation used could look a lot like the parts of proof assistants that automate proofs.