> we can't solve the halting problem or verify program correctness We can't solve halting problem or verify program correctness for all programs. For a large s

> we can't solve the halting problem or verify program correctness We can't solve halting problem or verify program correctness for all programs. For a large subset of all programs, you are able to do both. This is a very important distinction. We even have verified C compilers (CompCert). Writing a verified service manager should be easier in comparison.