Seconded, the “least upper bound” method for constructing the reals that I know about is… …Dedekind cuts.

What do you mean by "the use of the Least Upper Bound"?

Software gets used for mission critical things all the time, with the same level of assuredness. What you are complaining about is that people making apps to show you the right advertisement or a website to watch pictures of cats sometimes is buggy and gets deployed without proper tests.

Meanwhile almost every medical device under the sun today has software, nuclear powerplants run on software, space missions use software, airplanes drive themselves and land through software, etc.

To be fair, I don't see why LP is still being used for many applications nowadays and not replaced, as it tends to be a brute force techniques.

From page two of the paper: "Low-period oscillators in Life, roughly p ≤ 15, can be found by playing with patterns by hand or using brute force computer searches. In 1996, David Buckingham demonstrated [6] using his “Herschel conduits” that one can construct oscillators with p ≥ 61 by sending signals around a closed track; the cutoff for systematically constructing oscillators was later improved to p ≥ 43, by Mike Playle’s discovery of the Snark [43]."

I find his scepticism about proof assistants like Lean a bit weird. Of course, there is never absolute certainty, but there are degrees. A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong, which is possible but less likely than a flaw in a proof that hasn't seen much scrutiny because it's rather unimportant (of course, "big" results get so much scrutiny that it's also very unlikely that they were wrong).