Totally Live Programming and Proving in Hazel - A Programming Environment Overview

Watch a Topos Institute Colloquium talk exploring the Hazel programming environment, the first totally live typed general-purpose programming system. Discover how Hazel implements error localization and recovery mechanisms based on language theory to ensure syntactically well-structured and meaningful editor states. Learn about the underlying theoretical foundations and see live demonstrations of key features including the editor, training mode, and stepper functionality that supports theorem proving capabilities. Explore the vision for a "computational commons" operating as a planetary-scale live program, along with ongoing research directions. Through examples and discussion, understand how Hazel bridges the gap between programming and proving while maintaining usability through structured editing patterns and continuous feedback mechanisms.