I think some people do, or at least try to, but my impression of the state of computer-assisted proofs and formal verification methods for programs is that they are still not very good because the problem is incredibly complex and we’ve basically only made it to the level of having FORTRAN-level tools. This is to say, we’re a bit better off than we used to be doing formal verification with assembly-level tools where you had to specify absolutely everything in very low-level terms, but mostly in ways that just make it easier to do that low-level work rather than having many useful abstractions to help us perform formal verification without having to understand the details of (almost) everything all the time.
To continue the analogy, things will get a little more exciting as we get C and then C++ level tools, but I think things won’t really explode and be appealing to many folks who don’t desperately need to do formal verification until we get to something like the Python/Ruby-level in terms of tooling.
This does suggest something interesting, though: if someone thinks more widely using formal verification is important, especially in AI, then a straight-forward approach is to work on improving formal verification tools to a point that they can build up the abstractions that will help people work with them.
I think some people do, or at least try to, but my impression of the state of computer-assisted proofs and formal verification methods for programs is that they are still not very good because the problem is incredibly complex and we’ve basically only made it to the level of having FORTRAN-level tools. This is to say, we’re a bit better off than we used to be doing formal verification with assembly-level tools where you had to specify absolutely everything in very low-level terms, but mostly in ways that just make it easier to do that low-level work rather than having many useful abstractions to help us perform formal verification without having to understand the details of (almost) everything all the time.
To continue the analogy, things will get a little more exciting as we get C and then C++ level tools, but I think things won’t really explode and be appealing to many folks who don’t desperately need to do formal verification until we get to something like the Python/Ruby-level in terms of tooling.
This does suggest something interesting, though: if someone thinks more widely using formal verification is important, especially in AI, then a straight-forward approach is to work on improving formal verification tools to a point that they can build up the abstractions that will help people work with them.