Christophe Gyurgyik

Why scheduling languages exist

What Hoare wants and Rice forbids

December 23, 2025

C.A.R. Hoare’s work “Recursive data structures” motivates a simple rule that good language design should abide by:

(1) Implementation details that don’t affect program correctness are syntactically inexpressible.

Codd’s relational model attempts to realize this: you declare what you want (projections, joins) and the implementation (e.g., join order) is determined by the optimizer. In practice, programmers still reason about implementation details, shaping queries to optimize well. Programming languages generally abandon (1) entirely, giving us:

(2a) Implementation details that don’t affect program correctness are syntactically expressible.

C++ is the obvious case, but even Haskell qualifies. You make explicit decisions about memory representation:

-- unboxed (raw machine integer)
foo :: Int# -> Int#
foo x = x +# 1#

-- boxed (heap-allocated, thunk-able)
foo :: Int -> Int
foo x = x + 1

These choices are semantically invisible but syntactically required for performance reasons. Scheduling languages like Halide and TACO take a different path:

(3) Implementation details that don’t affect program correctness are confined to a separate language.

In Halide, you write the algorithm once as a pure functional description, and then separately write a schedule specifying optimizations such as tiling and parallelism. The schedule does not change the program semantics, only how the compute is performed. This separation is enforced syntactically.

// algorithm
f(x) = a(x) * b(x);

// schedule
f.parallel(x);

Why not just achieve (1) with a sufficiently clever compiler? Because determining which details “don’t affect correctness” requires deciding program equivalence (in general, Rice’s theorem forbids this). Scheduling languages today sidestep the problem for a small domain. They don’t ask the compiler to discover semantics-preserving transformations, they provide a language for the programmer to express them, while guaranteeing by construction that only semantics-preserving transformations are expressible.

There’s more to say about scheduling languages (e.g., encapsulation benefits, ergonomic costs), but that’s for another post. For now, (1) is the ideal, (3) is the pragmatic alternative when optimal performance is desired.