Enriching our interfaces with programs and proofs through automatic
diagramming. Diagrams are often compositional and structurally regular,
just like the objects they represent, be it data structures, proof terms,
algebraic objects, execution traces, or so on. Diagrams can compute and be
computed with.
Diagrams evolve systematically with steps of reasoning or execution.
But our diagramming tools today don’t take advantage of
any of this—we draw diagrams individually and ad hoc, letting go of the
conceptual diagram the moment we have its concrete rendering. How might we
instead specify a schema of diagrams, whose instances can be
automatically created from the objects being represented? How might we treat
diagrams as evolving computational objects separate from their renderings? How might we
codify æsthetic preferences to make automatic diagrams also
automatically pretty?
