> My reason: code can be checked objectively. I can run it and confirm it works.

Running the code only confirms that it works with the precise input, in the precise environment, under the precise circumstances you run it under. It doesn’t ensure that the code is correct. Thinking through the code, on the other hand, lets you consider all possible cases. It’s the difference between experiment and (mathematical) proof.

For an objective correctness proof, using a formal language is indispensable.