Although the first definition of "finite dimensional" is usually "there is a finite basis", this isn't the only way to characterise finite dimensional vector spaces and often a different way to characterise them can lead to a more elegant statement and proof of the theorem under consideration.
A vector space is finite dimensional if it is isomorphic to some Euclidean space. This is quite close to the notion of a basis and it is obvious that choosing such an isomorphism is tantamount to choosing a basis. However, it explains one of the roles of bases as explained in Greg's answer: to make an abstract vector space look like Euclidean space (and thus also make abstract linear transformations look like matrices).
There's Todd Trimble's definition in this question which relates finite dimensionality to duality.
A definition that doesn't use a "there exists" property (which implies that at some point you might want to make a choice) starts in the category of locally convex topological vector spaces, wherein a LCTVS is finite dimensional if it is a nuclear Banach space.
This is particularly relevant to the definition of trace, since a space $V$ is nuclear if every continuous linear map $V \to E$, where $E$ is a Banach space, is trace class. Thus if $V$ is nuclear and Banach, every continuous linear map $V \to V$ must admit a trace.
A vector space is finite dimensional if its exterior algebra has finite grading. Moreover, it has dimension $n$ if $\Lambda^n V$ is 1-dimensional. Thus we only need to know what 1-dimensional means for this to work.
In so far as defining trace is concerned, if one accepts that there is a way of defining determinants that doesn't involve defining bases (say, by using the top exterior power) then one can equally well define trace by differentiating the determinant:
$$ \frac{\det(I + tA) - 1}{t} \to \operatorname{Tr} A $$
Basically, choosing a basis is evil and should only be done when no-one is watching you and with proper precautions. More seriously, my answer to the original question "when to choose a basis" is:
- When you need to do a computation (as Greg says)
- When you want to convince yourself that a particular result is true before setting about the task of finding an elegant proof thereof.
Edit: I've thought of two more reasons to choose a basis:
- When the question is already evil.
- To avoid complicated convergence issues in Hilbert spaces: basically (pardon the pun), it's really easy to see when a sequence in which the terms are pairwise orthogonal converges so orthonormal bases (and orthonormal families) allow one to separate out the messy convergence from the elegant geometry.
