I agree with what <PERSON> has written. But also have a much simpler answer: In practice softwares engineers typically don't even try to check for correctness of their programs, they simply don't, they typically don't even write down the conditions that define when the program is correct.
There are various reasons for it. One is that most software engineers don't have the skills to clearly formulate problems mathematically nor they know how to write correctness proofs.
Another one is that defining correctness conditions for a complex software system (specially a distributed one) is a very difficult and time consuming task. They are expected to have something that seems to work in matter of weeks.
Another reason is that the correctness of a program depends on many other systems written by others which again so not have clear semantics. There is a <PERSON>'s law that essentially says if your library/service has an observable behavior (not part of its contract) someone will eventually depend on it. That essentially means the idea of developing software in modular form with clear contracts like lemmas in mathematics does not work in practice. It gets worse in languages in which reflection is used. Even if a program is correct today it might break down tomorrow when someone does some trivial refactoring in one of its dependencies.
In practice what typically happens is that they have tests. 904
Tests act as what is expected from the program. Everytime a new bug is found, they add tests to catch it. It works to some extend, but it is not a correctness proof.
When people don't have the skills to define correctness nor write correct programs nor expected to do so and doing so is rather difficult it is no surprise that softwares are not correct.
But note also that at the end in better places software engineering is done by code review. That is the author of a program has to convince at least one other person that the program works correctly. That is the point some informal high level arguments are made. But again typically nothing close to a clear rigorous definition of correctness or proof of correctness happens.
In mathematics people are focused on correctness. In software development there are many things that a programmer needs to care about and there are trade offs between them. Having a bug-free software or even a good definition of correctness (with requirements changing over time) is an ideal, but it has to be traded off against other factors and one of the most important among them is time spent on developing it by existing developers. So in practice in better places the goal and processes are mitigating the risk of bugs as much as feasible rather than making the software bug-free. 634