Thanks for gathering these thoughts here! I recently stumbled on them and got pulled into the post.
Small objection I’d like to make: You write that spec tooling most likely needs to be solved before any of the other problems become solvable, but I think it’s worse than that, because better tooling conserves the problem and relocates it.
Formalization splits one hard question (is this true of the world) into two:
Does it follow from the spec? (mechanically checkable)
Does the spec capture the world? (not checkable from inside, like ever?)
This seems to want for a shift into what a research program aimed at specifications should target: an exploration of validation (is it the right thing?) rather than verification (does it do the thing right?).
Also, knowing when a check tests for the property it claims to be about instead of passing for some other reason connects to vacuities in formal verification.
I agree with everything you’ve said! (If this is a research program you want to work on, please email me, and I will connect you with very well funded people working on these problems.)
Thanks for gathering these thoughts here! I recently stumbled on them and got pulled into the post.
Small objection I’d like to make: You write that spec tooling most likely needs to be solved before any of the other problems become solvable, but I think it’s worse than that, because better tooling conserves the problem and relocates it.
Formalization splits one hard question (is this true of the world) into two:
Does it follow from the spec? (mechanically checkable)
Does the spec capture the world? (not checkable from inside, like ever?)
This seems to want for a shift into what a research program aimed at specifications should target: an exploration of validation (is it the right thing?) rather than verification (does it do the thing right?).
Also, knowing when a check tests for the property it claims to be about instead of passing for some other reason connects to vacuities in formal verification.
I agree with everything you’ve said! (If this is a research program you want to work on, please email me, and I will connect you with very well funded people working on these problems.)