I agree with Elizabeth's answer and Brian Conrad's philosophy: avoid bases in theorem statements if possible, and use them sparingly for proofs.
More generally, when a definition of something says "something exists" (like a finite basis!), then at some point in your theory you'll essentially have to "choose" one of those things in order to complete a proof.
The definition of "finite-dimensional" means "a finite basis exists", so there's really no way around it. To illustrate this, we could work with "finite length as a k-module" as an alternative equivalent definition of finite dimensional vector space, but this just means "A finite maximal chain of vector subspaces exists," and what you find is that somewhere early in the foundations you have to "choose" such a chain in order complete a proof.
Edit: I'm not suggesting here that there are no equivalent characterizations of finite dimensional vector spaces; rather, I'm claiming that proving some of the properties of finite-dimensional vector spaces will involve the existence of "choices" in some way or another (as a trivial example, the property of having a finite basis). Of course making this claim rigorous and proving it would be a lot of work, but unfortunately I think the same is true for its negation.
