I’ve talked to a former grad student (fiddlemath, AKA Matt Elder) who worked on formal verification, and he said current methods are not anywhere near up to the task of formally verifying an FAI. Does MIRI have a formal verification research program? Do they have any plans to build programming processes like this or this?
I don’t know anything about MIRI research strategy than is publicly available, but if you look at what they are working on, it is all in the direction of formal verification.
After speaking to experts in formal verification of chips and of other systems, and they have confirmed what you learned from fiddlemath. Formal verification is limited in its capabilities: Often, you can only verify some very low-level or very specific assertions. And you have to be able to specify the assertion that you are verifying.
So, it seems that they are taking on a very difficult challenge.
I’ve talked to a former grad student (fiddlemath, AKA Matt Elder) who worked on formal verification, and he said current methods are not anywhere near up to the task of formally verifying an FAI. Does MIRI have a formal verification research program? Do they have any plans to build programming processes like this or this?
I don’t know anything about MIRI research strategy than is publicly available, but if you look at what they are working on, it is all in the direction of formal verification.
After speaking to experts in formal verification of chips and of other systems, and they have confirmed what you learned from fiddlemath. Formal verification is limited in its capabilities: Often, you can only verify some very low-level or very specific assertions. And you have to be able to specify the assertion that you are verifying.
So, it seems that they are taking on a very difficult challenge.