It's not clear that we couldn't prove arbitrary non-trivial properties (including halting) about *any application we actually care about*, though.
For example, type systems (if properly abused) let you prove all sorts of interesting properties about global data flow (e.g., the property "no string ever goes from the user to the database without being sanitized"). There's no good reason why the behavior of your X server, kernel, web server, browser, etc. should ever be *uncomputable*.
Large-scale proofs about programs are very hard, but that's a tools problem, not a deep conceptual abyss where no-one should ever even try to tread. (And we'd probably have better tools -- and programming languages -- if people were less scared of the abyss.)