From the paper: "Interestingly, reduced versions of the decidability problem have produced a fruitful area of re-search: formal verification, whose objective

From the paper: "Interestingly, reduced versions of the decidability problem have produced a fruitful area of re-search: formal verification, whose objective is to produce techniques to verify the correctness of computer programs and ensure they satisfy desirable properties (Vardi & Wolper, 1986). However, these techniques are only available to highly restricted classes of programs and inputs, and have been used in safety-critical applications such as train scheduling. But the approach of considering restricted classes of programs and inputs cannot be useful to the containment of superintelligence. Superintelligent machines, those Bostrom is interested in, are written in Turing-complete programming languages, are equipped with powerful sensors, and have the state of the world as their input. This seems unavoidable if we are to program machines to help us with the hardest problems facing society, such as epidemics, poverty, and climate change. These problems forbid the limitations im-posed by available formal verification techniques, rendering those techniques unusable at this grand scale."