Ez nem funkcionalis programozas, hanem egy theorem provernek a hasznalata. Ezzel csinaltak a helyessegbizonyitast. Az egy dolog, hogy a Coq az egy funkcionalis nyelven van implementalva, de ez nem jelent semmit. Barmilyen mas ekvivalens theorem proverrel mukodik a dolog.
Van Javaban irt theorem prover is, a Jape.
Van C++-ban irt theorem prover is, a z3, a Microsoft Research csinalja.