Why programming can't be fully formalized

One of the questions in computer science is whether programming can be fully formalized. On one hand, programming languages themselves are highly formal systems, defined by precise syntactic and semantic rules that enable machines to execute instructions deterministically. On the other hand, the act of programming involves much more than execution: it requires capturing human intent, reasoning about correctness, and ensuring alignment between abstract requirements and concrete behavior. While formal methods such as type theory, Hoare logic, and model checking have advanced the ability to reason rigorously about code, programming as a whole resists complete formalization.

The reason lies in the nature of software itself.