### Course of Lectures on

• First-order logic
• Set Theory
• $\lambda$-calculus
• Type Theory

## Formal Methods

Mathematical proofs checked by computers.

### The Pentium FDIV bug

• Thomas Nicely, a professor of mathematics at Lynchburg College, had written code to enumerate primes, twin primes, prime triplets, and prime quadruplets.
• Nicely noticed some inconsistencies in the calculations shortly after adding a Pentium system to his group of computers
• After eliminating other factors he reported the issue to Intel.
• This was a bug in the pentium chip due to missing entries in the lookup table used by the floating-point division circuitry.
• This bug had escaped testing.