The closest thing that comes to mind is total functional languages- the compiler doesn't deal with complexity classes, but it does prove termination. It's mostl

The closest thing that comes to mind is total functional languages- the compiler doesn't deal with complexity classes, but it does prove termination. It's mostly used in dependently-typed languages and theorem provers so they can prove the type checker will terminate.