It's not complete - addition and multiplication are not defined, nor even "number". Instead, it's properties of commutativity, associativity, distributivity, identities and inverses, and it's astonishing how far that takes us.
I really enjoyed this approach, but it has omissions: details like equality transitivity (things equal to something are equal to each other), and there's deliberate gaps (like using 0.a=0 twice in a proof before being proven, while claiming a comsequence).
I'd like full rigour, a treatment I could code, without need of mathematical maturity to paper-over abbreviations.
This is a big ask: I also want this detail without tedium; to retain the joie de vivre of Spivak, without gaps. The fun of building, like a construction set or building blocks.
Any recommendations? (perhaps I'll have to write it myself)
