4 ms·

I don't know that that's necessarily a fair characterisation. I've never seen any Coq syntax before a moment ago but it doesn't look wildly dissimilar to Haskel

I don't know that that's necessarily a fair characterisation. I've never seen any Coq syntax before a moment ago but it doesn't look wildly dissimilar to Haskell or Idris.

keithnz 8y ago
Hard to make any kind of fair comparison, but given the context, AOC2018, and the many many solutions in many languages, I think its reasonably fair to compare it to all of those and make a judgement on how it stacks up. It seems like it's being offered up for that specific comparison. Just for reference, another HNer offered up the following in python for inspection https://www.michaelfogleman.com/aoc18 https://www.michaelfogleman.com/aoc18 There are other posted solution sets on HN if you search... Now of course, lots of very different languages with different goals and philosophies. Hard to make a fair comparison, but, still I'm making a subjective comparison. The Coq code just does not seem compelling.
- intertextuality 8y ago
  How can you make a comparison from a glance when 1) python was explicitly made to be easy to read (English like) and 2) it’s absurdly common to see python code as opposed to Coq? Of course it’s possible it won’t make sense if you’re unfamiliar with the syntax or style. That’s like saying Haskell or Erlang are uncompelling from a brief glance, which ignores the benefits of using those languages.
  - keithnz 8y ago
    well, I gave the python as an example, there are more examples in most languages.... including Haskell. I have been programming ~40 years and have tried a lot of different languages in that time (not coq, but I have read about it and am curious about practical uses of it). There is no article with this repo, no explanations, I'm just saying I see nothing compelling... I'm completely willing to listen to a compelling argument for why I'd write Coq code and how theorem proving capabilities are worthwhile and how this code demonstrate it.
    - jolux 8y ago
      Functional programming languages, Gallina included, are far simpler and more regular in their grammars than imperative and object-oriented languages. It seems a bit off-the-wall to suggest that the Coq implementation isn't "compelling" without knowledge of how the language works or its design goals. To be clear, these design goals are not identical to Python's, which could be stated crudely as clarity and readability. As a brief aside, I've often encountered the claim that these goals make Python "English-like." For the grand failures achieved by pursuing such a mistake, one need look no further than COBOL and AppleScript. Python is clear and readable because it is relatively consistent, concise, and reads like how we are taught to expect pseudo-code to read, not because it reads like an English sentence. It could be argued that Coq's goal in the syntax and semantics department is mathematical clarity, which is somewhat different than the kind of clarity Python pursues. Mathematical clarity favors terseness, simplicity, and consistency above all else, because these features are necessary to express complicated ideas succinctly and unambiguously. As an argument in favor of this definition of clarity over Python's, I submit that programming correctly in a formal sense is quite difficult to do without tools that encourage it as Coq and other languages operating at the level of generality of the calculus of constructions do. Most statically typed languages do not have type systems powerful enough to express the properties that Coq can, and among those that do, I'm not sure any are syntactically simpler. Coq indeed sacrifices what is for a lot of traditionally trained programmers (myself included) the immediate familiarity of imperative pseudocode that Python expresses so well. What is gained is a highly general yet simple set of tools which can prove things about programs that are simply impossible with other tools. I would also argue that once the syntax is learned and the terseness adjusted to that Coq code is easy to read as well, and that the tradeoff for me is worth the learning period, but you may have different needs and priorities. I am intrinsically interested in rigorous formulations of software correctness, and I realize that makes me a bit more odd than the average programmer.
gameswithgo 8y ago
the solutions appears to take an order of magnitude more code than Haskell but Coq is also proving correctness so that seems expected
- bunderbunder 8y ago
  A fairer comparison would be Haskell code plus a complete suite of tests.
  - hiker 8y ago
    No suite of tests is complete enough to replace a proof. Unless the domain is finite and the tests exhaust all values in it.
    - melling 8y ago
      Out of curiosity, are there any studies that compare error rates among languages? How much is gained by going from say, Java to Haskell, or from Haskell to Coq?
      - fiddlerwoaroof 8y ago
        There's this, according to which Clojure does nearly as well as Haskell or Scala: https://jaxenter.com/programming-languages-defect-prone-report-138065.html https://jaxenter.com/programming-languages-defect-prone-repo...

I don't know that that's necessarily a fair characterisation. I've never seen any Coq syntax before a moment ago but it doesn't look wildly dissimilar to Haskell or Idris.

keithnz 8y ago

Hard to make any kind of fair comparison, but given the context, AOC2018, and the many many solutions in many languages, I think its reasonably fair to compare it to all of those and make a judgement on how it stacks up. It seems like it's being offered up for that specific comparison. Just for reference, another HNer offered up the following in python for inspection https://www.michaelfogleman.com/aoc18 https://www.michaelfogleman.com/aoc18 There are other posted solution sets on HN if you search... Now of course, lots of very different languages with different goals and philosophies. Hard to make a fair comparison, but, still I'm making a subjective comparison. The Coq code just does not seem compelling.

intertextuality 8y ago
How can you make a comparison from a glance when 1) python was explicitly made to be easy to read (English like) and 2) it’s absurdly common to see python code as opposed to Coq? Of course it’s possible it won’t make sense if you’re unfamiliar with the syntax or style. That’s like saying Haskell or Erlang are uncompelling from a brief glance, which ignores the benefits of using those languages.
- keithnz 8y ago
  well, I gave the python as an example, there are more examples in most languages.... including Haskell. I have been programming ~40 years and have tried a lot of different languages in that time (not coq, but I have read about it and am curious about practical uses of it). There is no article with this repo, no explanations, I'm just saying I see nothing compelling... I'm completely willing to listen to a compelling argument for why I'd write Coq code and how theorem proving capabilities are worthwhile and how this code demonstrate it.
  - jolux 8y ago
    Functional programming languages, Gallina included, are far simpler and more regular in their grammars than imperative and object-oriented languages. It seems a bit off-the-wall to suggest that the Coq implementation isn't "compelling" without knowledge of how the language works or its design goals. To be clear, these design goals are not identical to Python's, which could be stated crudely as clarity and readability. As a brief aside, I've often encountered the claim that these goals make Python "English-like." For the grand failures achieved by pursuing such a mistake, one need look no further than COBOL and AppleScript. Python is clear and readable because it is relatively consistent, concise, and reads like how we are taught to expect pseudo-code to read, not because it reads like an English sentence. It could be argued that Coq's goal in the syntax and semantics department is mathematical clarity, which is somewhat different than the kind of clarity Python pursues. Mathematical clarity favors terseness, simplicity, and consistency above all else, because these features are necessary to express complicated ideas succinctly and unambiguously. As an argument in favor of this definition of clarity over Python's, I submit that programming correctly in a formal sense is quite difficult to do without tools that encourage it as Coq and other languages operating at the level of generality of the calculus of constructions do. Most statically typed languages do not have type systems powerful enough to express the properties that Coq can, and among those that do, I'm not sure any are syntactically simpler. Coq indeed sacrifices what is for a lot of traditionally trained programmers (myself included) the immediate familiarity of imperative pseudocode that Python expresses so well. What is gained is a highly general yet simple set of tools which can prove things about programs that are simply impossible with other tools. I would also argue that once the syntax is learned and the terseness adjusted to that Coq code is easy to read as well, and that the tradeoff for me is worth the learning period, but you may have different needs and priorities. I am intrinsically interested in rigorous formulations of software correctness, and I realize that makes me a bit more odd than the average programmer.

gameswithgo 8y ago

the solutions appears to take an order of magnitude more code than Haskell but Coq is also proving correctness so that seems expected

bunderbunder 8y ago
A fairer comparison would be Haskell code plus a complete suite of tests.
- hiker 8y ago
  No suite of tests is complete enough to replace a proof. Unless the domain is finite and the tests exhaust all values in it.
  - melling 8y ago
    Out of curiosity, are there any studies that compare error rates among languages? How much is gained by going from say, Java to Haskell, or from Haskell to Coq?
    - fiddlerwoaroof 8y ago
      There's this, according to which Clojure does nearly as well as Haskell or Scala: https://jaxenter.com/programming-languages-defect-prone-report-138065.html https://jaxenter.com/programming-languages-defect-prone-repo...