Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste. Malheureusement, la machine utilise une arithmétique dite flottante, qui a ses contraintes. Ainsi, chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. Ce cours montrera tout d'abord la façon dont l'ordinateur calcule, mais aussi comment compenser ou tirer partie de ces erreurs. Il présentera ensuite la notion de preuve formelle qui permet de s'assurer de la correction d'un théorème mathématique et de sa preuve. Avec cela, on pourra produire des preuves d'algorithmes qui utilisent l'arithmétique des ordinateurs.