This always is an issue I take with people saying how certain technology is impossible due to <insert proof reducing technology to halting problem>. Type checking, code optimization, automatic proofs, etc. That's short-sighted.
As long as you reduce the power of your technology from "yes/no" to "yes/no/don't know" you're good to go.
Some optimizations may be impossible to apply in general due to the halting problem. But as long as you realize that the optimizer might return "I don't know if I can apply this", you can conservatively apply the optimization in the cases where the optimizer actually is sure.
Same for type checking. You can add a compiler warning: "Could not automatically prove type correctness.". Done. Now you can automatically check 99% of the cases where there are no halting problem issues, and leave the remaining 1% to the humans.
As long as you reduce the power of your technology from "yes/no" to "yes/no/don't know" you're good to go.
Some optimizations may be impossible to apply in general due to the halting problem. But as long as you realize that the optimizer might return "I don't know if I can apply this", you can conservatively apply the optimization in the cases where the optimizer actually is sure.
Same for type checking. You can add a compiler warning: "Could not automatically prove type correctness.". Done. Now you can automatically check 99% of the cases where there are no halting problem issues, and leave the remaining 1% to the humans.
Don't let perfect be the enemy of the good.