Since the time if Hyparco, it was known that the motion of celestial bodies is approximately given by epicycles.
In modern language, expressed in Fourier series of a few frequencies, which we now call quasi-periodic.
The advent of celestial mechanics raised the question of whether these motions are compatible with the laws of mechanics. The resonances in quasi-periodic motion could destroy each other. A great lore of formal computations and expansions was developed
for 300 years. On the other hand, the first proofs of persistence of quasi-periodic motions appeared only in the 1950's (Kolmogorov-Arnold-Moser theory).
With the use of computers and the need of applications, it has become important to know whether KAM theory can yield results applicable to problems of technological interest.
We will describe several results by many people that show that one can develop proofs that lead to efficient algorithms and which give confidence in the results.
Perhaps more importantly, the implementations permit to explore the boundaries and lead to beautiful conjectures.