Why do you think Haskell is fine as long as the system "isn't important enough to merit lots of manual verification"? That sounds puzzling to me. I'd say one thing complements the other: automatic and manual verification seems the best option.
Is lazy evaluation your biggest issue with Haskell? How about languages like ML or OCaml, which are arguably safer than "restricted C++" and do not default to lazy evaluation?
Or is GC your main problem with these languages? This would rule out most dynamically typed languages as well.
Anyways, you might want to read the stack overflow article on this subject: