A Type-Theoretic Commons for Trustworthy Human-AI Collaboration

Summary

Cyrus Omar presents a vision for a live type-theoretic computational commons: a shared code environment where humans and swarms of AI agents make verifiable progress on parallel tasks. Drawing on the Hazel programming environment, the design keeps incomplete programs analyzable and executable by representing missing code as typed holes, allowing feedback to continue past syntax and type errors. Hazel also supports probes, live values, graphical notations, direct manipulation, and incremental recomputation so small edits reuse unaffected execution and type information. Omar argues that AI agents face many of the same feedback problems as human programmers, including type-error gaps, recompilation costs, execution delays, and large textual logs, while also needing rapid re-contextualization because a new agent does not retain prior work. Hazel’s AI Assistant therefore operates through a structured semantic action language rather than a shell, enabling semantic search, contextualization, fine-grained edits, and inline runtime feedback. For human review, the talk describes a narrativized change-tour system that organizes pull-request hunks into an exhaustive explanation. At larger scale, Omar proposes tree-based CRDT editing with code relocation, Unison-style content-addressed versioning, and support for multiple code versions without immediate canonicalization. Security is addressed through type-theoretic object capabilities: task-specific capability signatures, shaped by humans or supervisor agents, would limit what an agent can access or change and could support proofs of policy correctness and information-flow guarantees for sensitive data. The long-term vision is a live network of programs, data, proofs, and graphical views that remains available during partial edits and can support collaborative scientific work, including climate modeling. The talk presents this as an ongoing research direction, with large-scale deployment and some interpreter and collaboration challenges still unresolved.