Achieving Correctness is really satisfying. however it is hard and difficult. IMOH this does in general polarize the scene (proving fanatics on one extreme and the other side who are not even testing the code)
IMHO flushing out what you are designing does help and goes along the way of having fewer bugs. one old relatively yet easy and accessible formal toolkit which helpful in flushing out process is Z notation . one of the accessible books, old yet an easy read and rewarding is
"Software Development with Z. A practical approach to formal methods in software engineering"
there are other notations developed later. but its simplicity and easiness even while scribling on paper or word processor gets me back to using it every now and then
I've a good track record of having my programs work without bugs, I don't think it's too hard. The way I work is to restrict myself to using building blocks that I know work well and produce correct results. For example: using state machines, never breaking out of a loop, tackling all the edge case before the body, using simple data structures, don't use inheritance or exceptions, don't interact with files natively, don't use recursion, etc. etc.
When I face a programming problem I map the solution to those simple building blocks, and If I can't I try to change the problem first.
Formal methods are hard if you want to prove the correctness of a hard algorithm, but you can almost always do without a hard algorithm and use something really basic instead, and for the basic things you don't need formal methods.
The people who write the most bugs in my experience do it because they don't fully understand the building blocks they're using, and rely on other things for correctness like the type checker or unit tests. They view code as a stochastic process, write code they don't fully understand and have accepted the resulting bugs as a fact of life.
"Software Development with Z. A practical approach to formal methods in software engineering"
https://archive.org/details/softwaredevelopm0000word/page/n1... .
there are other notations developed later. but its simplicity and easiness even while scribling on paper or word processor gets me back to using it every now and then