4 ms·

any reason to prefer Coq to Agda? And remind me what is the advantage over Haskell?

ufo 10y ago
Coq is more of a proof assistant than it is a general purpose programming language.
wyager 10y ago
Coq and Agda are both based on dependent types, but Agda is more of an in-progress research language whereas Coq is currently quite useful for doing proofs in practice. Haskell doesn't have full support for dependent types (yet). The Haskell community is very cautious with adding features that make type inference undecidable (like dependent types), so what people do is gradually add type system features onto GHC and then gate them behind feature flags. So you can do some of the things you can do in Agda in Haskell (like GADTs, kind promotion, limited type functions, etc.) but not everything. The advantage of Haskell's conservative approach is that it's actually very useful for writing programs, whereas Coq is only really meant for writing proofs and Agda is more of a research testbed than a production language.
- mitchty 10y ago
  Even when Haskell gets dependent types, they won't be quite as powerful as what agda/coq/idris have with the termination checks I believe. Which is fine, I don't think that many people want to program via proofs for everything. I'd say Idris is the closest to a useful general purpose programming language with proofs. At least that I've found so far, unless isabelle is? Not used it just came across it a while back and have to have a look. https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html
  - deleted 10y ago
    [deleted]
Jweb_Guru 10y ago
People actually use Coq to do useful things (this is kind of harsh to Agda but whatever). Haskell isn't really the same kind of thing (I mean, ostensibly you could write programs in Coq, and there are some extractors to other languages, but you generally use it as a proof assistant; by contrast, writing proofs in Haskell doesn't really work unless you happen to want to prove free theorems).

ufo 10y ago

Coq is more of a proof assistant than it is a general purpose programming language.

Coq and Agda are both based on dependent types, but Agda is more of an in-progress research language whereas Coq is currently quite useful for doing proofs in practice. Haskell doesn't have full support for dependent types (yet). The Haskell community is very cautious with adding features that make type inference undecidable (like dependent types), so what people do is gradually add type system features onto GHC and then gate them behind feature flags. So you can do some of the things you can do in Agda in Haskell (like GADTs, kind promotion, limited type functions, etc.) but not everything. The advantage of Haskell's conservative approach is that it's actually very useful for writing programs, whereas Coq is only really meant for writing proofs and Agda is more of a research testbed than a production language.

mitchty 10y ago
Even when Haskell gets dependent types, they won't be quite as powerful as what agda/coq/idris have with the termination checks I believe. Which is fine, I don't think that many people want to program via proofs for everything. I'd say Idris is the closest to a useful general purpose programming language with proofs. At least that I've found so far, unless isabelle is? Not used it just came across it a while back and have to have a look. https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html
- deleted 10y ago
  [deleted]

Jweb_Guru 10y ago

People actually use Coq to do useful things (this is kind of harsh to Agda but whatever). Haskell isn't really the same kind of thing (I mean, ostensibly you could write programs in Coq, and there are some extractors to other languages, but you generally use it as a proof assistant; by contrast, writing proofs in Haskell doesn't really work unless you happen to want to prove free theorems).