Then allow partial functions too. Maybe even require them to be tagged as such. (Is that within the capabilities of Zig's programmable type system?)

I don't mind escape hatches - as long as they're visible/greppable in the source code. You can always write undefined/error/panic/trace directives while you're coding, then come back and remove them later.

I would love a language that distinguishes functions (pure mathematical constructs) from procedures (imperative constructs that map in a predictable way to the instruction set).

This feels like the direction Algebraic Effects might take us.