You don't need to solve the halting problem to write provably correct software (that is, software that conforms to a formal specification). The halting problem (and Rice's theorem) come into play when you are trying to deduce things about arbitrary programs written in turing complete languages.

It's like the difference between being able to express proofs in maths, versus having a method of deciding the validity of arbitrary propositions. We can certainly write programs that we can we can prove things about, but given an arbitrary program, we can't always tell whether it will do the right thing.

It was "solved" in 1940 (proven in 1967) by the simply typed lambda calculus.

They didn't say it had to be Turing complete.

It's not about turing completeness. Deducing arbitrary properties of programming written in primitive recursive languages is also undecidable. This is why type inference in dependently typed languages is undecidable.