> If you formalize, you'll end up with one rigorous definition

Can't you just formalize both definitions and pick the one to work with based on what you want to do? Surely the only obstacle here is the time and effort it takes to write the formalization?

Or, alternatively, just because you've formalized the advanced calculus version doesn't mean you need to use the formalization when teaching basic calculus. The way we've proven something and the way we teach that something don't have to be the same.

That's very helpful and clear, thank you