Comment by nickpsecurity

You create a subset or model of what's computable. Then, work in it. You might also prove refinements from high- to low-level forms.

Interestingly, we handle static analysis the same way by using language subsets. The larger chunk is unprovable. So, we just work with what's easy to analyze. Then, wrap it in types or contracts to use it properly.

And plenty of testing for when the specs are wrong.