Since the widespread adoption of the IEEE-754 standard for floating-point arithmetic in the mid-1980s, numerical accuracy arguments have enjoyed a period of relative stability: paper proofs of numerical accuracy applied to concrete implementations without the need to explicitly restate underlying arithmetic assumptions. This stability enabled the development of standardized algorithmic interfaces such as the Basic Linear Algebra Subprograms (BLAS), which decoupled high-level reasoning about algorithmic properties from the low-level intricacies of designing optimized implementations, while leaving floating-point assumptions implicit. As a result, many well-known accuracy results are conditional on the IEEE-754 semantics for floating-point arithmetic, even when those conditions are not stated explicitly.

However, this silent semantic contract is breaking down: driven by the need for increased speed and reduced communication and energy costs, floating-point hardware and arithmetic formats are becoming increasingly diverse, and informal accuracy arguments no longer transfer reliably. In this talk, I argue that making arithmetic assumptions explicit, formal, and parameterized is now necessary infrastructure, not just an academic exercise. Building on mechanized floating-point semantics and algorithm-level specifications for numerical linear algebra, type systems and proof assistants can restore a principled separation of concerns, future-proofing numerical accuracy arguments in a rapidly evolving floating-point landscape.