Cyrus Omar: 'Totally Live Programming and Proving in Hazel'

Topos Institute Colloquium, 29th of August 2024.
———
This talk will review progress on the Hazel programming environment and its underlying theoretical developments. Hazel is the first totally live typed general-purpose programming environment, meaning that it deploys error localization and recovery mechanisms, rooted in language-theoretic developments, that ensure that every editor state is syntactically well-structured and statically and dynamically meaningful. The talk will review the underlying theory and include a live demonstration of various Hazel features, including its editor, training mode, and its stepper, which is forming the basis for ongoing work on a Hazel-based theorem prover. The talk will also discuss various other ongoing and future directions of interest to the community, including our vision for a "computational commons" that operates like a planetary-scale live program.