Development Roadmap

From notebook to proof.

Presheaf evolves from a Vision Pro notebook application into a mathematically grounded reactive spatial notebook system with a formally specified, verified execution model. The phases below trace that path.

Phases 2–5 · Building the runtime

Phase 2

Reactive spatial notebook foundation

Notebook cells form an explicit dependency graph — like Pluto.jl — while staying Jupyter-compatible. A reactive engine propagates updates through both 2D and 3D cells.

Dependency graph
Topological scheduling
Dirty propagation
Cycle detection
Partial recomputation
Cancellation
Live scene outputs
.ipynb compatibility

Foundation

Phase 2.5

Workspace & interaction redesign

Notebook becomes navigation; objects become the workspace. HIG-compliant windows, volumes and ornaments replace mixed-content clutter — pinning, grouping, remembered layouts, and 60–90 FPS at scale.

visionOS HIG

Stage 3A

Spatial runtime architecture

Notebook, rendering and execution split apart: SceneController, RendererRegistry, ExecutionCoordinator, DependencyManager.

Stage 3B

Rendering pipeline

Renderer plugins, shared resource caches, GPU pooling, LOD, streaming — and ornament occlusion resolved.

Stage 3C · 3D

Interaction & persistence

Transform gizmos, snapping, measurements, linked brushing, undo/redo — plus workspace persistence, autosave, versioning, and export to .ipynb, USD and JSON.

Cross-highlighting
Camera bookmarks
Document diffs
CRDT-ready

Phase 4

Formal presheaf semantics

The notebook is formalized in Lean as a presheaf over a dependency category — objects, morphisms, restriction maps, gluing and sheaf conditions — with every runtime object traceable to a Lean definition.

Lean · proofs

Phase 4B

Pulto helpers integration

The Python helper package becomes the semantic companion — MIME types, serialization and dependency metadata upgraded to emit objects matching the Lean model, with JSON schemas and automatic notebook validation.

Phase 5

Production runtime contract

A canonical Draft 2020-12 JSON Schema and a runtime contract every notebook must satisfy — validated identically across Swift, Python and TypeScript, with automatic legacy migration.

Schema validation
Graph validation
Property tests
Migration tests

Cross-language contract

Post-Phase 5 · Research horizon

Phase 6

Plugin SDK

Extensibility for third-party spatial renderers, execution backends and notebook object types.

Phase 7

Distributed execution

Reactive execution across local and remote kernels, with collaborative editing and scheduling.

Phase 8

Categorical optimization

Using the presheaf formalization to optimize dependency graphs, incremental recompute and storage.

Phase 9

Formal verification

Proving Swift and Python faithfully implement the Lean specification and satisfy the runtime contract.

End state