Program termination

The proof assistants Coq and Isabelle allow the user to define functions, then export those functions to some functional programming language. In Coq, you can export to OCaml, Haskell, or Scheme (documentation.) In Isabelle, you can export to Standard ML, OCaml, Haskell, or Scala (documentation).

The vast majority of programs we want to write, eventually terminate. There are of course exceptions, such as Web servers. Termination proofs are tedious, but most are done in Coq and Isabelle automatically. If the automatic termination prover fails, you can always supply your own measure function, to either Coq or Isabelle, to prove the function terminates after all.