Conference Presentation, Product Demonstration
Trustworthy Human-AI Collaboration in a Live Type-Theoretic Computational Commons
- Predicts that as AI systems reach thousands of tokens per second, human performance will shift from generation speed to tool feedback bottlenecks, necessitating timely, quick feedback loops and inline feedback to enable surgical edits that reduce token usage.
- Plans to develop collaborative tree editing systems with commutativity properties to resolve code relocation conflicts and intends to combine these foundations with Unison's content-addressed versioning, where code is never deleted, to support parallel versioning and cleanups for AI agents.
- Envisions a computational commons consisting of a network of live programs edited by humans and AI, where edits causing syntax or type errors do not crash the system, requiring incremental compilation and execution to manage rapid agent editing volumes.
- Outlines plans for large-scale climate modeling sabbaticals to build world models as live programs that link domain-specific data, such as ocean temperatures, while aiming to eliminate multi-year waits between big model point releases.
- Proposes using object capability systems and information flow control within the Hazel tool language to establish baseline provably correct policies, ensuring sensitive data like patient emails reaches only designated charts.
- Anticipates that the distinction between development and deployment will blur in dynamic environments, potentially requiring legacy versions to persist permanently to allow reference to old versions within a single codebase without settling on a single canonical version.
- Expects reduced adoption costs for new languages via AI-assisted library creation, allowing the community to prioritize building necessary infrastructure over managing existing software engineering network effects.
- Details plans to add theory improver capabilities to Hazel based on an Isabel-style design to facilitate proofs throughout the system for abstract review, while developing a Foreign Data Interface with pluggable components to act as a JIT to Spark for large datasets.
- Projects that future AI agent swarms will require tools addressing gaps in editor services and trained to aggressively check their work, with translational research succeeding either through sufficient engineering support or by spurring competitors to build similar solutions.
- Foresees a dynamic environment where humans monitor reports and manipulate computed elements when agents encounter uncertainty, such as leaving sliders for visual parameters, while maintaining the ability to refer to historical versions within a unified codebase.