Languages like Prolog and Haskell represent different views on the relation between logic and computation. Prolog models computation as proof search, whereas Ha

Languages like Prolog and Haskell represent different views on the relation between logic and computation. Prolog models computation as proof search, whereas Haskell models it as proof normalization. In the former case your program basically consists of a bunch of formulas that are used as assumptions in an attempt to answer a query at runtime. With Haskell, your program consists of terms, which correspond directly to proofs under the Curry-Howard isomorphism. From the type theory perspective, with functional programming languages like Haskell the programmer writes terms (proofs) of some given type (formula), whereas with logic programming it's the runtime that tries to answer whether a given type is inhabited (i.e., if a proof exists). I'm being a bit sloppy here in that I'm disregarding the differences between classical and intuitionistic logics, although the former as well have been studied in type theory via their double negation translations. I think Girard's ludics, among other goals, tried to unify these two views, although I know too little about it. Finally, note Coq, like Haskell, models computation as proof normalization, although it's design goals are very different from Haskell.