Reasoning with equations is a central part of mathematics. Typically we think of solving equations but another role they play is to define algebraic structures like groups or vector spaces. Equational logic was formalized and developed by Birkhoff in the 1930s and led to a subject called universal algebra. Universal algebra was used in formalizing concepts of data types in computer science. In this talk I will present a quantitative analogue of equational logic: we write expressions like s =_ε t with the intended interpretation "s is within ε of t".

For decades, Moore’s Law and its partner Dennard Scaling have driven technology trends that have enabled exponential performance improvements in computer systems at manageable power dissipation.  With the slowing of Moore/Dennard improvements, designers have turned to a range of approaches for extending scaling of computer systems performance and power efficiency.  Unfortunately, these scaling gains come at the expense of degraded hardware-software abstraction layers, increased complexity at the hardware-software interface, and increased challenges for software relia