Unfortunately I still have a soft spot for beautiful writing. The "point" often sticks better when it is expressed eloquently. Having to think a little bit to get to the point also helps with absorbing it, at least in my experience.
> I am slowly replacing the Cotton/Hazlitt translation with a contemporary one and adding new notes
So I would assume that the essay you're talking about is from the earlier Cotton translation and has still not been replaced.
This is the first time I've seen AI being used to "modernize" old texts, and it works wonderfully in this case; though a bit of the old-timey charm is lost imo. I used to read a translation that I'd found in my university library which I enjoyed a lot. Very readable but still retained the "feel" of a 16th century book. I don't recall the translator unfortunately.
Everything you are looking for is provided in the Epilogue of Spivak. For instance, in chapter 28, you will be able to show that 0a = 0 in any field. In chapter 29, you will rigorously define the reals as well as the operations on them. You will also show that they form a complete ordered field, which allows you to use the results from chapter 28. In chapter 30 you will show that all complete ordered fields are "essentialy the same" as the real numbers---i.e., the real numbers are "unique."
At the moment I'd advise not worrying much about the construction of the reals. Ideas such as limits, continuity, differentiation, integration, and even fields are much more important for later mathematics and applications (abstract algebra, topology, geometry, physics) than the construction of the reals. Constructing the reals is pretty much something you do a couple of times (traditionally once with Dedkind cuts, as in Spivak, and once more with Cauchy sequences) and then never think about again.
Edit: I'm not sure what you mean by "something I could code." If you want something that you could type in a proof assistant you might have some luck looking at the mathlib library of Lean https://leanprover-community.github.io/mathlib4_docs/Mathlib....