The post shows how the technique introduced in that paper, “internal guarded recursion,” can be used not only in a lightweight formal way, but just in everyday programming as a “back of the envelope” technique to quickly figure out when recursive functional programs terminate and when they go into infinite loops.
I think the approach is very simple to use, and hope people can come up with lots of classes of examples where it can be helpful.
Based on that mangled (<*>) operator in the initial Haskell example:
newtype Later a = Later a deriving Functor
instance Applicative Later where
pure = Later
Later f < *> Later x = Later (f x)
-- ^^^^
…it could be yet another site-formatting error.
As for the concept itself: it looks like a “small-footprint” variant of total programming (as opposed to actual total programming, which bans implicit general recursion outright) - nicely done.