@andrejbauer In Metamath we develop reals way before we do anything with rings (or rigs, or groups, or any other algebraic structures). Which I guess is to my taste, but I try not to be too dogmatic about whether one or the other is better. (In this case the order of topics was decided WAY before I was working on the project).