Computer Arithmetic and Formal Proofs: Floating-point Algorithms with the Coq System explores floating-point arithmetic, a tool that is ubiquitous in modern computing as the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and cause numerous failures. This book explains how to avoid this and increase confidence in floating-point software by using the computer-assisted verification of correctness proof (the Coq proof assistant), the tool that is comprehensively discussed throughout this book.