Implementation and Synthesis of Math Library Functions

Explore a groundbreaking approach to implementing and synthesizing math library functions in this 20-minute video presentation from POPL 2024. Discover MegaLibm, a domain-specific language designed to address the challenges of developing accurate and efficient implementations of functions like exp, sin, and log. Learn how MegaLibm's safe, modular, and tunable features enable developers to detect mathematical errors, build implementations incrementally, and separate high-level and low-level decision making. Gain insights into how this innovative tool allows for interactive development, compilation, testing, and tuning of implementations, as well as the integration of tools like Sollya and type-directed synthesis. Understand how MegaLibm can express state-of-the-art math library implementations with comparable speed and accuracy to original C code, while also enabling the synthesis of variations and from-scratch implementations with minimal guidance.