Super cool in-progress programming language: DCS, a functional programming language with a totality checker but not dependent types (unlike the proof assistants that usually have totality checkers). The idea is to allow divergence via a Div effect monad (cf. Haskell’s IO) while having the bulk of the language guaranteed to terminate. One of the big selling points is that the totality checker works for divide-and-conquer strategies, which Coq etc generally don’t.
It can do this because it’s based on some very complex type-level machinery where recursive functions are actually (I hope I’m using these words correctly) Mendler-inductive functor algebras. Totality checkers require that arguments to recursive calls be smaller than the original argument, but normally enforce that purely based on the syntax of constructors which means they can’t go through the function calls required for divide and conquer splits. Here, the idea is whenever there would be recursion, it instead uses an opaque type variable and an extra function parameter to enforce that the call can only be to something “recursable”, and takes a fixed point so that it ends up back at the original recursive type. (I might try and write more about these if anyone is interested, or to figure out if I actually understand it or if I’m just nodding my head along.)
I don’t know if it’s possible to pour enough syntactic sugar onto that concept to make it actually usable as a language. but the examples of programs in the language are way more readable than the version displayed in the paper, so it honestly might be. The list file in the stdlib has both quicksort and mergesort, and if you look past the decision to use Greek letters instead of keywords and the limited pattern-matching it doesn’t look that far off a normal recursive function.
My biggest question, though, is how it’s possible to take a fixed point of the algebra without risking nontermination. If your totality checker isn’t total, what’s the point?