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....