Source code organizes a program as expressions and declarations, which a compiler can represent as an abstract syntax tree (AST). Some compilers introduce a further abstraction of the computation as a graph. Nodes represent operations, while connections record how values pass between them and how execution proceeds. Yet these connections can leave the full scope of conditions governing a computation implicit. Developers may then need defensive checks, rely on compiler hacks, pragmas, and implementation-specific code to maintain those conditions as the program evolves. Our thesis is that a hypergraph more faithfully represents complex computation across all targets by making joint constraints inherent to its structure, with an overall less burdensome design-time API. Our Program Hypergraph (PHG) extends our Semantic Graph with relations that connect across an operation's participants, their dependencies, and the invariants they must preserve. Joint resolution in the graph guides lowering into standard Multi-Level Intermediate Representation (MLIR). Satisfiability modulo theories (SMT) checks intrinsic to the graph discharge applicable proof obligations. Supporting information remains available until the decisions that require it are complete. As a primary benefit, verification follows from the rules used to construct and transform the graph. For properties established this way before execution, the generated program needs no added runtime checks, no 'boxing' or 'tagging' or other managed runtime support. We develop this account through geometric algebra, shared-memory capacity, and spatial placement, distinguishing structural guarantees from numerical and resource obligations that require further evidence. The proposed integration makes the same information available at design-time, so engineers can inspect the consequences of a choice before it becomes an implementation constraint.

翻译：暂无翻译