> 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.