Watch a 56-minute computer science seminar where Princeton University's Eugene Higgins Professor Andrew Appel explores formal verification techniques for numerical methods in scientific computing. Learn about machine-checked program verification connecting low-level programs to algorithm specifications, with a focus on numerical integration of differential equations and solving linear systems. Discover how formal verification tools can be applied across different domains while ensuring both algorithm implementation correctness and mathematical accuracy. Gain insights from Appel's collaborative research with Cornell and Michigan universities on developing provably correct numerical computation methods. Understand the importance of domain-specific mathematics in proving algorithm correctness and the challenges of implementing fully verified numerical methods for scientific applications.