11 ms·

Advent of Code 2018, in Coq

149 points by szemet 8y ago

elizabeth_olu 8y ago
www.elizabethblog.com.ng
BenMorganIO 8y ago
Coq, can't get enough of it!
tombert 8y ago
I never liked Coq's name because I'm immature, but it really is magic software in my eyes. The level of downright objectivity that you get with it makes it feel so bulletproof. I know functional languages are slowly starting to adopt dependent types, and you can get reasonable certainty of correctness with property-based testing, but Coq just feels kind of universal. If the proof passes, so will your code. I really wish I could get my employer to sign off on me using it for a real project.
- quickthrower2 8y ago
  Good enough, with bugs is what makes the real money unfortunately.
  - dan-robertson 8y ago
    I don’t really like this trope. The goal of a programming in Coq would, I suppose, be to shift debugging time from after compilation succeeds to before, with the hope that the compiler will direct one towards the bugs and they will be easier to find. I don’t think this is always a win. I think it is a win if what you write must be very reliable, but it seems less obvious that the advantage would still exist as the required reliability decreases. Remember that bug Coq had when if you used more than 256 parameters in a constructor you could prove anything? I suppose one could say Coq is good enough, with bugs.
    - bunderbunder 8y ago
      What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios. Maybe that's FUD on my part; I've only read Coq code and never written any of my own. In any case, at least the way I'm thinking of it, it's not that good enough with bugs is what makes the money. It's more a question of proportionality: It doesn't make sense to spend $100 to guard against a $5 bug. I don't think Coq leaves much room for being pragmatic about test coverage like that.
      - Swizec 8y ago
        > What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios. Isn't the same true for static typing? One small business requirement changes, you change a foundational type, and suddenly all your code needs to adapt. Of course this is true with dynamic typing too, but at least you don't know.
        deleted 8y ago
        [deleted]
        bunderbunder 8y ago
        I guess. My experience has been that it's more a case with, for lack of a better term, "old school" OOP. SOLID helps a lot with that sort of thing. Avoiding inheritance like the plague helps a lot. I slightly hate that I said old school, because Smalltalk-style tell-don't-ask helps a lot. I think that the idiomatic ways of structuring code in the ML family of languages help the most, because they tend to be pretty radical about limiting scope of visibility. But they also tend to make more of a muddle of things than they're worth in algol-style languages.
        dmitriid 8y ago
        > Isn't the same true for static typing? One small business requirement changes, you change a foundational type Business changes are usually changes in logic, not in types. So it's mostly "our cashback is now calculated in percentage of the sum, not as a fixed sum" etc. Of course, this may still have repercussions through the entire system. I don't know how it would work in Coq (I don't know Coq :) ).
  - rtpg 8y ago
    good enough without bugs makes you a lot of money and also lets you build something with a much smaller team. I don't think Coq is the way forward (I don't think "code that makes money" has many interesting provable properties in itself along those axes) but being able to ship stuff that's pretty close to bug-free will get you far
- OnlyOneCannolo 8y ago
  It's pronounced closer to "coke".
  - tom_mellior 8y ago
    No. The software Coq is pronounced like the French word "coq", which has a short o like the English "cock" and unlike the long o in the English "coke". https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr This is certainly the only pronounciation in the French formal methods community, where Coq comes from. It is also the standard pronounciation in the international formal methods community. I have never heard anyone pronounce it like "coke". See for example Adam Chlipala at about 5:40 here: https://www.youtube.com/watch?v=4DYVJdHMV5k https://www.youtube.com/watch?v=4DYVJdHMV5k Benjamin Pierce has a slightly longer o here, but it doesn't sound to me like it's deliberately pronounced differently from "cock": https://www.youtube.com/watch?v=KKrD4JcfW90 https://www.youtube.com/watch?v=KKrD4JcfW90 And here is Andrej Bauer: https://www.youtube.com/watch?v=COe0VTNF2EA https://www.youtube.com/watch?v=COe0VTNF2EA I know from rare comments like yours that some prudish Americans pronounce it "coke", some deliberately, others apparently because they have been fooled by the first group. But this seems to be a very small minority.
    - dragonwriter 8y ago
      > The software Coq is pronounced like the French word "coq", Yes, but... > which has a short o like the English "cock" No, it doesn't. The sound it has isn't a common English vowel sound at all; it is closer to the vowel sounds in “cuck” and “cook” than the one in “cock”, but not exactly either of those, either. In fact of the four (those two, plus coke and cock), the “o” in “cock” is the one most Americans would find it most distinct from, I would think. > https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr Yeah, none of those pronounce it with the vowel sound in English “cock”. > I know from rare comments like yours that some prudish Americans pronounce it "coke", It's not prudish, its a common way Americans that haven't mastered French pronunciation approximate the unaccented French “o” irrespective of context.
      - tom_mellior 8y ago
keithnz 8y ago
Looking at the code, and having done AOC2018 and having looked at a lot of solutions in various languages, I don't really like the code, the solutions are really not obvious and it all seems like a syntactic mess.
- 0xADEADBEE 8y ago
  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.
syrak 8y ago
Hello there. I'm the author of this repo. Not as much has been going on in that project as I would have liked. It certainly doesn't help that: - The standard library is actually quite poor. A lot of basic functions must be implemented from scratch, and then you'll also want to write proofs about them. - I had to reinvent IO in Coq. - Most AOC problems are actually not that well-suited for formal verification. (It's certainly no fault of the AOC organizer!) In particular, a lot of them basically ask you to simulate some system which doesn't have particularly interesting properties, so the implementation itself is often the best specification of the problem, and the main point of using a language like Coq is lost. I did find some interesting problems though. For example, day 5 was a simple rewriting system and the question was to find the normal form of some starting string. Well, who's to say that the answer is unique? In this case it's easy enough to convince oneself that the given system actually is confluent, but I set out to prove it formally (and (re)learned a few things about rewriting systems on the way). (c.f., Confluent_react_steps, react_steps_injective, in day_05_common.v)

149 points by szemet 8y ago

elizabeth_olu 8y ago

www.elizabethblog.com.ng

BenMorganIO 8y ago

Coq, can't get enough of it!

tombert 8y ago

I never liked Coq's name because I'm immature, but it really is magic software in my eyes. The level of downright objectivity that you get with it makes it feel so bulletproof. I know functional languages are slowly starting to adopt dependent types, and you can get reasonable certainty of correctness with property-based testing, but Coq just feels kind of universal. If the proof passes, so will your code. I really wish I could get my employer to sign off on me using it for a real project.

quickthrower2 8y ago
Good enough, with bugs is what makes the real money unfortunately.
- dan-robertson 8y ago
  I don’t really like this trope. The goal of a programming in Coq would, I suppose, be to shift debugging time from after compilation succeeds to before, with the hope that the compiler will direct one towards the bugs and they will be easier to find. I don’t think this is always a win. I think it is a win if what you write must be very reliable, but it seems less obvious that the advantage would still exist as the required reliability decreases. Remember that bug Coq had when if you used more than 256 parameters in a constructor you could prove anything? I suppose one could say Coq is good enough, with bugs.
  - bunderbunder 8y ago
    What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios. Maybe that's FUD on my part; I've only read Coq code and never written any of my own. In any case, at least the way I'm thinking of it, it's not that good enough with bugs is what makes the money. It's more a question of proportionality: It doesn't make sense to spend $100 to guard against a $5 bug. I don't think Coq leaves much room for being pragmatic about test coverage like that.
    - Swizec 8y ago
      > What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios. Isn't the same true for static typing? One small business requirement changes, you change a foundational type, and suddenly all your code needs to adapt. Of course this is true with dynamic typing too, but at least you don't know.
      - deleted 8y ago
        [deleted]
      - bunderbunder 8y ago
        I guess. My experience has been that it's more a case with, for lack of a better term, "old school" OOP. SOLID helps a lot with that sort of thing. Avoiding inheritance like the plague helps a lot. I slightly hate that I said old school, because Smalltalk-style tell-don't-ask helps a lot. I think that the idiomatic ways of structuring code in the ML family of languages help the most, because they tend to be pretty radical about limiting scope of visibility. But they also tend to make more of a muddle of things than they're worth in algol-style languages.
      - dmitriid 8y ago
        > Isn't the same true for static typing? One small business requirement changes, you change a foundational type Business changes are usually changes in logic, not in types. So it's mostly "our cashback is now calculated in percentage of the sum, not as a fixed sum" etc. Of course, this may still have repercussions through the entire system. I don't know how it would work in Coq (I don't know Coq :) ).
- rtpg 8y ago
  good enough without bugs makes you a lot of money and also lets you build something with a much smaller team. I don't think Coq is the way forward (I don't think "code that makes money" has many interesting provable properties in itself along those axes) but being able to ship stuff that's pretty close to bug-free will get you far
OnlyOneCannolo 8y ago
It's pronounced closer to "coke".
- tom_mellior 8y ago
  No. The software Coq is pronounced like the French word "coq", which has a short o like the English "cock" and unlike the long o in the English "coke". https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr This is certainly the only pronounciation in the French formal methods community, where Coq comes from. It is also the standard pronounciation in the international formal methods community. I have never heard anyone pronounce it like "coke". See for example Adam Chlipala at about 5:40 here: https://www.youtube.com/watch?v=4DYVJdHMV5k https://www.youtube.com/watch?v=4DYVJdHMV5k Benjamin Pierce has a slightly longer o here, but it doesn't sound to me like it's deliberately pronounced differently from "cock": https://www.youtube.com/watch?v=KKrD4JcfW90 https://www.youtube.com/watch?v=KKrD4JcfW90 And here is Andrej Bauer: https://www.youtube.com/watch?v=COe0VTNF2EA https://www.youtube.com/watch?v=COe0VTNF2EA I know from rare comments like yours that some prudish Americans pronounce it "coke", some deliberately, others apparently because they have been fooled by the first group. But this seems to be a very small minority.
  - dragonwriter 8y ago
    > The software Coq is pronounced like the French word "coq", Yes, but... > which has a short o like the English "cock" No, it doesn't. The sound it has isn't a common English vowel sound at all; it is closer to the vowel sounds in “cuck” and “cook” than the one in “cock”, but not exactly either of those, either. In fact of the four (those two, plus coke and cock), the “o” in “cock” is the one most Americans would find it most distinct from, I would think. > https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr Yeah, none of those pronounce it with the vowel sound in English “cock”. > I know from rare comments like yours that some prudish Americans pronounce it "coke", It's not prudish, its a common way Americans that haven't mastered French pronunciation approximate the unaccented French “o” irrespective of context.
    - tom_mellior 8y ago

keithnz 8y ago

Looking at the code, and having done AOC2018 and having looked at a lot of solutions in various languages, I don't really like the code, the solutions are really not obvious and it all seems like a syntactic mess.

0xADEADBEE 8y ago
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.

syrak 8y ago

Hello there. I'm the author of this repo. Not as much has been going on in that project as I would have liked. It certainly doesn't help that: - The standard library is actually quite poor. A lot of basic functions must be implemented from scratch, and then you'll also want to write proofs about them. - I had to reinvent IO in Coq. - Most AOC problems are actually not that well-suited for formal verification. (It's certainly no fault of the AOC organizer!) In particular, a lot of them basically ask you to simulate some system which doesn't have particularly interesting properties, so the implementation itself is often the best specification of the problem, and the main point of using a language like Coq is lost. I did find some interesting problems though. For example, day 5 was a simple rewriting system and the question was to find the normal form of some starting string. Well, who's to say that the answer is unique? In this case it's easy enough to convince oneself that the given system actually is confluent, but I set out to prove it formally (and (re)learned a few things about rewriting systems on the way). (c.f., Confluent_react_steps, react_steps_injective, in day_05_common.v)