This will be mainly an expository talk on quantifier elimination and decision algorithm for the first order theory of reals (due to A. Tarski). Quantifier elimination is very important for the geometry of semialgebraic sets. Its algorithmic nature gives effectiveness results almost for free. Of course one has to work more if one wants more precise information than recursive bounds, for instance.This question of effectiveness will be illustrated with some examples, notably the Hauptvermutung which states that the semialgebraic triangulation of a semialgebraic set is essentially unique.