Embed Notice

@julesh I think that's basically what the Calculus of Inductive Constructions (as used in Coq / Lean) provides.

The syntax only allows recursion on structurally smaller arguments.

Recursion on inductive types is always well-founded and you can define inductive types for a well-foundedness relation, which basically means that all provably total functions are definable.

The syntax ranges from "reasonable" (any obviously structural recursion requires no annotiation) to "custom proof required".