Future-Proofing Numerical Accuracy with Formal Specifications
summary
Argues that making floating‑point assumptions explicit and parameterized preserves accuracy as hardware and formats diversify. Builds LA proof, a library of mechanized floating‑point semantics and accuracy theorems in rock that connects BLAS‑style functional specs to C via VST, proves sound, compositional bounds and the convergence of a Jacobi solver, with theoretical bounds roughly a factor of two above observed errors. Works for low precision and IEEE‑754 rounding; stochastic rounding and non‑IEEE formats remain unsupported and need formalization.
AI-written summary · about
chapters (12)
- 0:00Future-proofing numerical accuracy
- 1:23Why numerical linear algebra works
- 4:32Role of BLAS in numerical linear algebra
- 9:09BLAS accuracy limitations
- 17:56Introducing LA Proof and formal specs
- 21:51Criteria for accuracy theorems
- 25:23Soundness and tightness in error bounds
- 27:08Jacobi method case study with LA Proof
- 32:42Future-proofing with stochastic rounding
- 35:54Opportunities in non-IEEE formats
- 38:25How Rocq community can help
- 41:04Q&A
related talks
51mFloating-Point Arithmetic on Deterministic Systems
01h 04mCross-Platform Floating-Point Determinism Out of the Box
02mWhen Computers Can't Math - Floating Point Rounding Error Explained
56mHow to Quickly Convert Floating-Point Numbers in C++
38mStrength in Numbers: Unums and the Quest for Reliable Arithmetic
23mPattern-Based Optimization (...)
01h 37mAn Overview of Program Optimization Techniques
26mFinite Difference Methods Fengshui: Alignment through a Mathematics of Arrays