4 ms·

Maybe I have the history wrong but it seems to me that researchers moved on from classical logic to lambda calculus and intuitionist Martin-Lof type theories an

by js8 8y ago

Maybe I have the history wrong but it seems to me that researchers moved on from classical logic to lambda calculus and intuitionist Martin-Lof type theories and associated programming languages (ML, Miranda, Ocaml, Haskell, Coq). Am I wrong in thinking that Coq for example can be considered a replacement of Prolog?

AnimalMuppet 8y ago
> Am I wrong in thinking that Coq for example can be considered a replacement of Prolog? I don't know if you're right or wrong about that. But Coq is about as "dead" as Prolog is. That is, it isn't used very much for real-world programming. It doesn't look like it's going to become more alive very soon, either. Even if Coq and Prolog can be considered as "in the same style/family", maybe the problem is that for most problems, most people just don't want to program that way?
- smadge 8y ago
  I suspect that most of programming languages in common use today started out as academic exercises that weren’t used for real-world programming and that most people didn’t enjoy programming in.
tom_mellior 8y ago
Both Coq and Prolog have something to do with logic, but that is where the similarities end. Other than this, they are apples and oranges. Prolog is a programming language whose execution is based on certain logical principles. Coq is a functional programming language, and and extra logic layer to prove things about programs written in its programming language. If you will, Prolog uses logic at "run time", while Coq uses logic at "compile time". Different things (and very different logics).
arnobastenhof 8y ago
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.
- deleted 8y ago
  [deleted]

by js8 8y ago

AnimalMuppet 8y ago

> Am I wrong in thinking that Coq for example can be considered a replacement of Prolog? I don't know if you're right or wrong about that. But Coq is about as "dead" as Prolog is. That is, it isn't used very much for real-world programming. It doesn't look like it's going to become more alive very soon, either. Even if Coq and Prolog can be considered as "in the same style/family", maybe the problem is that for most problems, most people just don't want to program that way?

smadge 8y ago
I suspect that most of programming languages in common use today started out as academic exercises that weren’t used for real-world programming and that most people didn’t enjoy programming in.

tom_mellior 8y ago

Both Coq and Prolog have something to do with logic, but that is where the similarities end. Other than this, they are apples and oranges. Prolog is a programming language whose execution is based on certain logical principles. Coq is a functional programming language, and and extra logic layer to prove things about programs written in its programming language. If you will, Prolog uses logic at "run time", while Coq uses logic at "compile time". Different things (and very different logics).

arnobastenhof 8y ago

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.

deleted 8y ago
[deleted]