3 ms·

Are there benefits in learning Coq for those who work mainly with general purpose programming?

by haolez 7y ago

tom_mellior 7y ago
It's fun, and it gives you new perspectives about how you might reason about program correctness in other languages as well, even if only informally in your head.
- seanwilson 7y ago
  Agree with that - I found it makes you write simpler code because you start thinking e.g. "hmm, if I write the algorithm this way, it would take forever to prove correct in Coq so it must be an overly complex approach". If you find it hard to justify robustly in your head why some code should work it's probably very difficult to prove formally which usually means there's a large surface area for bugs too. I found a big aspect of proving program correctness was formulating programs in a way first that made them easier to prove. It makes you cringe at mutable state and loops with nontrivial conditions.
- philzook 7y ago
  It is fun and useful if you're interested in formal program correctness or mathematics. Maybe it's a useful bitter pill to swallow even if you're not, but the world is a wide and wonderful place, and maybe Coq isn't the best use of your time. I think it's really interesting though, so it doesn't hurt to give it a looksy.
jhanschoo 7y ago
If you aren't doing formal verification of programs, the other main use case of Coq would be using it to assist with coining a new domain-specific language, and proving that the language meets certain requirements. If you have a concurrent program you can also try encoding a fragment with simplified semantics in Coq and prove the correctness of the program in Coq. https://softwarefoundations.cis.upenn.edu/current/plf-current/Smallstep.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... Here is an example of that for a toy language.
darzu 7y ago
IMO, yes. Similar to the benefits of learning Haskel as a Javascript programmer, there are ideas better embodied in Coq that translate to all languages. For example, the idea of strengthening & weakening the inputs/outputs of your lemmas, functions, or any abstraction is really central Coq. Constantly there is a tension between weakening your preconditions so your abstraction is easier to apply while also strengthening your postconditions so you get more leverage from you abstraction, or doing just the opposite so that implementing the abstraction is possible. After working with Coq almost exclusively for a year and then returning to regular programming, I find this is a concept I come back to constantly. It applies to any language. One example is creating library API preconditions & postconditions such that the API is useful to the caller but not so tight that there's no room to change implementation details as the maintainer. With API contracts in particular, it's usually possible to strengthen a postcondition and weaken a precondition without breaking compatibility so it's helpful to start with weaker postconditions and stronger preconditions to give you that flexibility. In regular languages, preconditions & postconditions is something that the language only helps you out partially. Even in Haskel this is true. Most of the contract is not enforced by the type system and can only be described in documentation. If your API takes in a "number", chances are there are bounds on what that number can be, e.g. non-negative or less than the length of the list. In Coq, all of this would be very explicit and machine enforced. When writing contracts now, I sometimes imagine what lemmas and witnesses I would have written or assumed in Coq and that helps me think about the trade offs. This concept often applies beyond APIs to the whole system architecture. What should that microservice require of its inputs and what guarantees can that storage system provide, etc.

Are there benefits in learning Coq for those who work mainly with general purpose programming?

by haolez 7y ago

Are there benefits in learning Coq for those who work mainly with general purpose programming?

It's fun, and it gives you new perspectives about how you might reason about program correctness in other languages as well, even if only informally in your head.

seanwilson 7y ago
Agree with that - I found it makes you write simpler code because you start thinking e.g. "hmm, if I write the algorithm this way, it would take forever to prove correct in Coq so it must be an overly complex approach". If you find it hard to justify robustly in your head why some code should work it's probably very difficult to prove formally which usually means there's a large surface area for bugs too. I found a big aspect of proving program correctness was formulating programs in a way first that made them easier to prove. It makes you cringe at mutable state and loops with nontrivial conditions.
philzook 7y ago
It is fun and useful if you're interested in formal program correctness or mathematics. Maybe it's a useful bitter pill to swallow even if you're not, but the world is a wide and wonderful place, and maybe Coq isn't the best use of your time. I think it's really interesting though, so it doesn't hurt to give it a looksy.

jhanschoo 7y ago

If you aren't doing formal verification of programs, the other main use case of Coq would be using it to assist with coining a new domain-specific language, and proving that the language meets certain requirements. If you have a concurrent program you can also try encoding a fragment with simplified semantics in Coq and prove the correctness of the program in Coq. https://softwarefoundations.cis.upenn.edu/current/plf-current/Smallstep.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... Here is an example of that for a toy language.

darzu 7y ago

IMO, yes. Similar to the benefits of learning Haskel as a Javascript programmer, there are ideas better embodied in Coq that translate to all languages. For example, the idea of strengthening & weakening the inputs/outputs of your lemmas, functions, or any abstraction is really central Coq. Constantly there is a tension between weakening your preconditions so your abstraction is easier to apply while also strengthening your postconditions so you get more leverage from you abstraction, or doing just the opposite so that implementing the abstraction is possible. After working with Coq almost exclusively for a year and then returning to regular programming, I find this is a concept I come back to constantly. It applies to any language. One example is creating library API preconditions & postconditions such that the API is useful to the caller but not so tight that there's no room to change implementation details as the maintainer. With API contracts in particular, it's usually possible to strengthen a postcondition and weaken a precondition without breaking compatibility so it's helpful to start with weaker postconditions and stronger preconditions to give you that flexibility. In regular languages, preconditions & postconditions is something that the language only helps you out partially. Even in Haskel this is true. Most of the contract is not enforced by the type system and can only be described in documentation. If your API takes in a "number", chances are there are bounds on what that number can be, e.g. non-negative or less than the length of the list. In Coq, all of this would be very explicit and machine enforced. When writing contracts now, I sometimes imagine what lemmas and witnesses I would have written or assumed in Coq and that helps me think about the trade offs. This concept often applies beyond APIs to the whole system architecture. What should that microservice require of its inputs and what guarantees can that storage system provide, etc.