Halide is a domain-specific language for building and optimizing numerical pipelines for applications in image processing, neural networks, and linear algebra. Its distinctive separation of what to compute — the algorithm — from the organization of that computation — the schedule — enables programmers to focus on the optimization of their programs without reasoning about loop index edge cases, concurrency issues, or portability. Halide then ensures memory safety through a bounds inference engine that determines safe sizes for every buffer in the generated code.

In this paper, we present the Halide language in a formal setting, provide semantics for every part and proofs of correctness for the scheduling directives, and define the bounds inference problem in terms of program synthesis. We believe this precision will bolster future work in extending Halide to support a broader computational model, assist validating the implementation against a formal specification, and inspire the design of new languages and tools that apply programmer-controlled scheduling to other domains.