3 ms·

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

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.

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.