> For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops. I'm not sure about CoC-the-abstract-calculus-on-paper, but I gu

> For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops. I'm not sure about CoC-the-abstract-calculus-on-paper, but I guess it cannot allow programs that lack a termination proof. Coq-the-concrete-implementation-of-CoC does allow some. Or not, depending how you look at it: What it will really do is infer a termination proof behind the scenes for certain simple cases, like iterating over a list and the recursive call always being on the tail of the current list. So everything has a termination proof in Coq, it's just that in simple cases you get it for free.