12 ms·

The C standard formalized in Coq

231 points by janvdberg 11y ago

xvilka 11y ago
Would be nice to use it for Frama-C. [1] http://frama-c.com http://frama-c.com
pron 11y ago
I would strongly encourage anyone interested in formal methods (and formal proofs in particular) but may be intimidated by dependent types, which serve as the basis for Coq (and are foreign not only to software developers but to most mathematicians as well) to give TLA+[1] a look. It is a decade younger than Coq (16 vs. 26), but simpler to use, much more gradual, and has had industry adoption pretty much since its inception. Instead of dependent types (in fact, TLA+ is untyped[2]) It is based on simple ZF set theory and logic, and should be immediately familiar to anyone who's taken even one logic (or discrete math) course in college. In addition to a proof assistant it has a good model checker, comes bundled in a nice (relatively speaking) IDE, and is easy to learn (with a thorough tutorial written by Leslie Lamport himself). TLA+ is also more widely used in the industry -- both hardware and software -- perhaps most notably in the software industry by Amazon, who use TLA+ to specify many of their AWS services. TLA+ is a formal specification (and verification) tool designed for engineers and used by engineers. Although, to be fair, neither tool is used by a large portion of the industry. EDIT: Removed potentially incendiary Lamport quote. EDIT: Changed an incorrect statement about Coq's use in the industry [1]: http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl... [2]: See Should Your Specification Language Be Typed? by Lamport and Paulson: http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-types.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
- fuklief 11y ago
  Coq is also used in industry, in particular by Airbus with the CompCert C compiler.
  - pron 11y ago
    Do Airbus engineers write Coq specifications or just use CompCert (a C compiler formally verified with Coq in academia)?
    - deleted 11y ago
      [deleted]
    - nmrm2 11y ago
      This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.
      - pron 11y ago
        > The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
        nmrm2 11y ago
        My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
- nmrm2 11y ago
  A note for the unitiated: There is a tension between TLA+ and Coq et al. (typified by statements such as "weird computer-science math") that is similar and maybe even rooted in to the sorts of culture wars that sprout up around programming languages (see [2] of parent's post for a perfect example of what I'm talking about...) The characterization in pron's post is decidedly biased toward TLA+ in a way that I think is unnecessary. A few correctives: * Coq has seen plenty of industry adoption. To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is wrong. * "Normal" mathematicians (not just "weird Computer Science-type" mathematicians, whatever that means...) have used and extolled the virtues of Coq as a tool as well as its theoretical foundations. See e.g., the univalent foundations project. Regardless, I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is. And if the goal is formalized mathematics, you're probably better off with Coq (and it's not even clear that the TLA+ community is interested in that sort of thing, independnet of results useful in the course of a program specification/verification task.) * If you're familiar with (esp. typed) functional programming, you might find Coq even easier to get into than TLA+. On both sides of the type theory vs sets/axioms divide, people should be careful not to confuse one's predispositions based upon educational background with the actual mental load of learning to use a tool. There is room for both of these tools (and more!) in the world. I don't understand why they have to be in competition. A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement!
  - unboxed_type 11y ago
    I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.
  - pron 11y ago
    > To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is disingenious. I never said that Coq is an academic toy. Some projects done in academia and used in the industry have been verified with Coq, but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). > I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is I've never said it is unreasonable, only that it is foreign to most engineers (as well as most academic CS people), or rather, more foreign than basic logic/set theory. I would say again that if you're comfortable with type theory, you might enjoy Coq better. If not, TLA+ would probably be more approachable. TLA+ has the added advantage of having a model checker, which is very useful when you don't have the resources required for a full proof, but still want a good confidence in the correctness of your algorithm. > A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement! Oh, absolutely! It's just that stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most. TLA+ is a good entry point to formal methods, even if you later choose to move to dependent-type approaches and tools.
- unboxed_type 11y ago
  Also take a look at this thread, were I briefly describe our experience of using all the spectre of verification tools. https://news.ycombinator.com/item?id=10220264 https://news.ycombinator.com/item?id=10220264
- random778 11y ago
  Would you advise one to start directly with TLA+ or work through some logic/discrete math seperately beforehand?
  - nmrm2 11y ago
    If you have had the equivalent of an undergraduate course on Discrete Mathematics you are probably fine; an introduction to logic course (covering e.g., soundness and completeness of propositional/first order logics) probably isn't necessary. There is a self-contained book; IMO chapter 1 gives a good overview of what you should be comfortable with: http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
  - agentultra 11y ago
    Not the author but a recent book I've read on the subject served as a gentle introduction for me: The Little Prover [0]. If you can get past the lisp syntax you can get through this book with an informal and incomplete education in set theory and an intuitive understanding of logic. [0] https://mitpress.mit.edu/index.php?q=books/little-prover https://mitpress.mit.edu/index.php?q=books/little-prover
  - pron 11y ago
    Lamport's tutorial (the TLA+ Hyperbook) as well as the old TLA+ book (Specifying Systems) -- both available freely on the TLA+ homepage -- cover all the math you need (which is little more than logical conjunction/disjunction/implication, the quantifiers for all/exists, and set membership/union/intersection). But it is perhaps better to be familiar with those simple concepts beforehand, although note that what you need is very, very basic. As nmrm2 said, there's no need for a full Discrete Math course (or a whole book).
- nickpsecurity 11y ago
  Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+. The topic is verification of compilers or imperative programs in C language. I don't know of anyone using TLA+ for that or advocating for it. It's mainly used as a lightweight approach in protocol verification. So, distributed apps not C code or compilers. Now, Coq has plenty of history in certified programming and compilation. There exists formalisms and models of most pieces of the puzzle. There are worked examples of certified compilers whose details and sometimes source are available for re-use. There's even already a verified C compiler other works are building on. It was used in EAL7-class JavaCard interpreters, database structures I believe, web services, and so on. Even outputs to robust Ocaml code. People needing to learn this stuff even have free books like Chlipala's: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ So, anyone trying to specify or formally verify compilers or algorithms have plenty of reason to choose Coq. It's actually one of the best tools for the job with HOL or Isabelle the other style. Field kind of diverges doing parallel work with them in imperative verification. Coq is possibly easier to use and seems to have more prior work to draw on in this. So, it's either the best or one of best tools for the job. TLA+ is for totally different jobs. Not relevant here.
  - throwaway999888 11y ago
    > Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+. pron has this habit of being negative and dismissive towards functional programming and related things, recommending non-FP alternatives instead. Which is fine, only that sometimes he's too trigger happy and just gives unsolicited advice without any build up or with weak topical relevance. Like here.
    - pron 11y ago
      I am not dismissive towards Coq (how can anyone be?), and my advice is neither less solicited nor less relevant than many other HN comments. But you are right that I sometimes try to correct what I see as a (strange) imbalance here on HN (which reflects neither the prevailing opinions in academia nor in the industry) regarding PFP and type theory. People unfamiliar with the topic might get the impression that PFP+type-theory is either the only or the most prevalent technique for software verification (or software correctness in general), while neither is the case. In exchange, I get to be the lucky target of various ad hominem attacks, so I guess I've earned my right to speak up :)
asmodian 11y ago
To an english speaker it sounds like the word for male genitalia. Doubt it's intentional. Care to clarify pronunciation? Edit: American here. I realize this is based on british english, which uses the word cock entirely differently.
- alex95 11y ago
  cock
- theGimp 11y ago
  Coq is French for rooster. Wiktionary has the pronunciation: https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg
- deleted 11y ago
  [deleted]
- jjgreen 11y ago
  It is pronounced "cock" which is (British) English for a male chicken, what an American might call a rooster. Not surprising, as cock is derived from the French _coq_.
  - asmodian 11y ago
    In USA, cock is pretty much just about penis. Another one I hear is fag / faggot, which is considered hate speech and grounds for immediate termination. I understand you just want to program. I knew the answer before you responded because I made the deliberate attempt to understand. Twitter gangs won't extend the same courtesy to you when their livelihood depends on stowing outrage over cheap gambits like that. These days in USA non-programmers can easily invoke code of conduct to have careers permanently ruined. Canadian harassment laws now cover disagreeing with females' sensibilities also can get you in jail.
    - mikegerwitz 11y ago
      I upvoted your original question because it is a legitimate one, whether others like it or not. I actually have gotten very few odd looks even from non-programmers when pronouncing "Coq" as "cock" _in the proper context_. "Use Coq" would probably yield a different out-of-context interpretation than "For problem X I think we should consider Coq. It allows ..." I don't think this is much of a problem in practice.
geon 11y ago
Heh. CH2O = formaldehyde
vinceyuan 11y ago
The font size on this page is very small. My eyes hurt when I read it on my non-retina 13-inch Macbook Pro (on low-resolution external monitor, it looks bigger.). Is it because I am not a native English speaker? Do native English speakers get used to this font size? Some websites including Hacker News use very small font size. Reddit's font size is bigger. I created a HN web reader ( http://hackernewsroom.com http://hackernewsroom.com ) with bigger font size (for myself and friends) to read titles and comments easily. But I can't change the font size of the original article. (Have to zoom in the page by pressing cmd+=)
- testtest 11y ago
  It might be because the font size is defined in the CSS in pixel units, instead of em, which is a point size (DPI dependent). http://www.w3.org/TR/REC-CSS2/syndata.html#length-units http://www.w3.org/TR/REC-CSS2/syndata.html#length-units If you have a problem reading text on the screen, I suggest you use something like Clearly extension that reformats pages with a much more reading-friendly style. You don't have to sign up to use this extension : https://evernote.com/clearly/ https://evernote.com/clearly/ You can also try to print the page into a PDF and read it like that.
  - wereHamster 11y ago
    Note that CSS pixels are not the same as physical pixels. Browsers are free to rescale CSS pixel values. Indeed, it's written in the document you linked to: > If the pixel density of the output device is very different from that of a typical computer display, the user agent should rescale pixel values. So actually 12px font should look about the same on all output devices, regardless of their physical DPI. But I agree that 12px is rather small for copy text.
    - Someone 11y ago
      12px font also could become very small in the future, if typical computer displays end up having high dpi. I guess a conforming browser should randomly sample computer displays before deciding how big 1px is. Serious version: I don't think text like that should make it into a standard.
alexbock 11y ago
One issue with this is that the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. The official standards mailing lists for C and C++ are constantly filled with issues regarding inconsistencies in the ISO standards, and for C++ at least people often resort to trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear. It might be a bit better with C, but I once tried to start implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly. There are so many pieces where you are just expected to know what they intend and what inconsistencies can be ignored because you're already familiar with the language that it would be difficult to call any one person's interpretation a formalization of the standard itself.
- thinkpad20 11y ago
  > the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. Interesting! If the standard is under-specified, then presumably this student must have had to fill in some of the holes themselves, or found a way to represent multiple interpretations simultaneously. > issues regarding inconsistencies in the ISO standards If the standards are inconsistent (in a logical sense), and this formalization is sufficiently complete, it should uncover those inconsistencies since they would amount to type errors in Coq. I wonder if the author had any of those difficulties. > trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear One of the effects a project like this could have is to make this (at least theoretically) unnecessary to do. > implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? I'm not sure what the C standard is but it must be quite a bit smaller. Regardless, it's a PhD thesis so the difficulty of the task isn't a reason not to attempt it :)
  - nly 11y ago
    > Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? The language specification itself is only about ~450 pages, the rest is library. It of course inherits all of the insanity of C on top of that (~170 pages of C language spec), which I'd argue brings a disproportionately large share of the pain. Alex's point is that the standard doesn't really begin to give you an idea how hard it is to write an implementation, or make decisions about everything that's unspecified or ambiguous.
sanxiyn 11y ago
Note that this formalization is substantially incomplete: check page 195. CH2O does not formalize variadic function, float, bit field, setjmp/longjmp. All of them are formalized in KCC. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics
- deleted 11y ago
  [deleted]
  - sanxiyn 11y ago
    No, I am referring to PDF page 195.
- redsymbol 11y ago
  That's true. The immediate-term impact is probably minimal, for the reasons you mention. However, this is a major accomplishment. As this work is built upon, its longer-term impact has the potential to be very significant.
  - sanxiyn 11y ago
    I agree it is a major accomplishment. I have doubts about its impact, because I am unsure whether it will be built upon. CH2O's main innovation is C standard (as opposed to C implementation) formalized in general purpose prover (as opposed to custom system). KCC formalized C standard, but not in general purpose prover. CompCert formalized in general purpose prover, but formalized implementation instead of standard. Formalizing in general purpose prover is useful because you can use all of math to prove runtime invariants. But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. For time when you want to prove abstractly to standard, this doesn't seem better than KCC. In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me.
    - baq 11y ago
      it's a phd thesis that advances state of the art. to me it feels you have expectations verging on, please excuse my wording, unreasonable.
JabavuAdams 11y ago
> Surprisingly, correctly describing the set of programs that have undefined behavior in a formal manner is the hardest part of formalizing C. Isn't this undecidable?
- obastani 11y ago
  I think that statement is referring to simply defining "undefined behavior", not actually determining whether a given program has undefined behavior.
- mikeash 11y ago
  Yes, but that doesn't mean you can't describe it. The halting problem is undecidable, but it's really easy to describe the set of programs that halt. I just described it right there! That quote is talking about defining the set, not determining whether a program is a member of the set (which is indeed impossible in the general case).
LukeHoersten 11y ago
awesome
rav 11y ago
In a sense, Robbert's thesis can be viewed as a more mathematically stringent (and thus arguably clearer) C11 specification. For instance, page 42 has the following mathematical gem: > The C11 standard defines the usual arithmetic conversions as a binary operation on integer types. This definition is complicated and contains some implicit duplication due to symmetry, which is inconvenient when proving properties. To improve the situation, we show that the usual arithmetic conversion of integer types τ_i and σ_i is a least upper bound τ_i ∪ σ_i in a join semi-lattice.

231 points by janvdberg 11y ago

Would be nice to use it for Frama-C. [1] http://frama-c.com http://frama-c.com

pron 11y ago

I would strongly encourage anyone interested in formal methods (and formal proofs in particular) but may be intimidated by dependent types, which serve as the basis for Coq (and are foreign not only to software developers but to most mathematicians as well) to give TLA+[1] a look. It is a decade younger than Coq (16 vs. 26), but simpler to use, much more gradual, and has had industry adoption pretty much since its inception. Instead of dependent types (in fact, TLA+ is untyped[2]) It is based on simple ZF set theory and logic, and should be immediately familiar to anyone who's taken even one logic (or discrete math) course in college. In addition to a proof assistant it has a good model checker, comes bundled in a nice (relatively speaking) IDE, and is easy to learn (with a thorough tutorial written by Leslie Lamport himself). TLA+ is also more widely used in the industry -- both hardware and software -- perhaps most notably in the software industry by Amazon, who use TLA+ to specify many of their AWS services. TLA+ is a formal specification (and verification) tool designed for engineers and used by engineers. Although, to be fair, neither tool is used by a large portion of the industry. EDIT: Removed potentially incendiary Lamport quote. EDIT: Changed an incorrect statement about Coq's use in the industry [1]: http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl... [2]: See Should Your Specification Language Be Typed? by Lamport and Paulson: http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-types.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...

fuklief 11y ago
Coq is also used in industry, in particular by Airbus with the CompCert C compiler.
- pron 11y ago
  Do Airbus engineers write Coq specifications or just use CompCert (a C compiler formally verified with Coq in academia)?
  - deleted 11y ago
    [deleted]
  - nmrm2 11y ago
    This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.
    - pron 11y ago
      > The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
      - nmrm2 11y ago
        My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
nmrm2 11y ago
A note for the unitiated: There is a tension between TLA+ and Coq et al. (typified by statements such as "weird computer-science math") that is similar and maybe even rooted in to the sorts of culture wars that sprout up around programming languages (see [2] of parent's post for a perfect example of what I'm talking about...) The characterization in pron's post is decidedly biased toward TLA+ in a way that I think is unnecessary. A few correctives: * Coq has seen plenty of industry adoption. To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is wrong. * "Normal" mathematicians (not just "weird Computer Science-type" mathematicians, whatever that means...) have used and extolled the virtues of Coq as a tool as well as its theoretical foundations. See e.g., the univalent foundations project. Regardless, I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is. And if the goal is formalized mathematics, you're probably better off with Coq (and it's not even clear that the TLA+ community is interested in that sort of thing, independnet of results useful in the course of a program specification/verification task.) * If you're familiar with (esp. typed) functional programming, you might find Coq even easier to get into than TLA+. On both sides of the type theory vs sets/axioms divide, people should be careful not to confuse one's predispositions based upon educational background with the actual mental load of learning to use a tool. There is room for both of these tools (and more!) in the world. I don't understand why they have to be in competition. A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement!
- unboxed_type 11y ago
  I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.
- pron 11y ago
  > To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is disingenious. I never said that Coq is an academic toy. Some projects done in academia and used in the industry have been verified with Coq, but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). > I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is I've never said it is unreasonable, only that it is foreign to most engineers (as well as most academic CS people), or rather, more foreign than basic logic/set theory. I would say again that if you're comfortable with type theory, you might enjoy Coq better. If not, TLA+ would probably be more approachable. TLA+ has the added advantage of having a model checker, which is very useful when you don't have the resources required for a full proof, but still want a good confidence in the correctness of your algorithm. > A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement! Oh, absolutely! It's just that stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most. TLA+ is a good entry point to formal methods, even if you later choose to move to dependent-type approaches and tools.
unboxed_type 11y ago
Also take a look at this thread, were I briefly describe our experience of using all the spectre of verification tools. https://news.ycombinator.com/item?id=10220264 https://news.ycombinator.com/item?id=10220264
random778 11y ago
Would you advise one to start directly with TLA+ or work through some logic/discrete math seperately beforehand?
- nmrm2 11y ago
  If you have had the equivalent of an undergraduate course on Discrete Mathematics you are probably fine; an introduction to logic course (covering e.g., soundness and completeness of propositional/first order logics) probably isn't necessary. There is a self-contained book; IMO chapter 1 gives a good overview of what you should be comfortable with: http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
- agentultra 11y ago
  Not the author but a recent book I've read on the subject served as a gentle introduction for me: The Little Prover [0]. If you can get past the lisp syntax you can get through this book with an informal and incomplete education in set theory and an intuitive understanding of logic. [0] https://mitpress.mit.edu/index.php?q=books/little-prover https://mitpress.mit.edu/index.php?q=books/little-prover
- pron 11y ago
  Lamport's tutorial (the TLA+ Hyperbook) as well as the old TLA+ book (Specifying Systems) -- both available freely on the TLA+ homepage -- cover all the math you need (which is little more than logical conjunction/disjunction/implication, the quantifiers for all/exists, and set membership/union/intersection). But it is perhaps better to be familiar with those simple concepts beforehand, although note that what you need is very, very basic. As nmrm2 said, there's no need for a full Discrete Math course (or a whole book).
nickpsecurity 11y ago
Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+. The topic is verification of compilers or imperative programs in C language. I don't know of anyone using TLA+ for that or advocating for it. It's mainly used as a lightweight approach in protocol verification. So, distributed apps not C code or compilers. Now, Coq has plenty of history in certified programming and compilation. There exists formalisms and models of most pieces of the puzzle. There are worked examples of certified compilers whose details and sometimes source are available for re-use. There's even already a verified C compiler other works are building on. It was used in EAL7-class JavaCard interpreters, database structures I believe, web services, and so on. Even outputs to robust Ocaml code. People needing to learn this stuff even have free books like Chlipala's: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ So, anyone trying to specify or formally verify compilers or algorithms have plenty of reason to choose Coq. It's actually one of the best tools for the job with HOL or Isabelle the other style. Field kind of diverges doing parallel work with them in imperative verification. Coq is possibly easier to use and seems to have more prior work to draw on in this. So, it's either the best or one of best tools for the job. TLA+ is for totally different jobs. Not relevant here.
- throwaway999888 11y ago
  > Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+. pron has this habit of being negative and dismissive towards functional programming and related things, recommending non-FP alternatives instead. Which is fine, only that sometimes he's too trigger happy and just gives unsolicited advice without any build up or with weak topical relevance. Like here.
  - pron 11y ago
    I am not dismissive towards Coq (how can anyone be?), and my advice is neither less solicited nor less relevant than many other HN comments. But you are right that I sometimes try to correct what I see as a (strange) imbalance here on HN (which reflects neither the prevailing opinions in academia nor in the industry) regarding PFP and type theory. People unfamiliar with the topic might get the impression that PFP+type-theory is either the only or the most prevalent technique for software verification (or software correctness in general), while neither is the case. In exchange, I get to be the lucky target of various ad hominem attacks, so I guess I've earned my right to speak up :)

asmodian 11y ago

To an english speaker it sounds like the word for male genitalia. Doubt it's intentional. Care to clarify pronunciation? Edit: American here. I realize this is based on british english, which uses the word cock entirely differently.

alex95 11y ago
cock
theGimp 11y ago
Coq is French for rooster. Wiktionary has the pronunciation: https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg https://en.m.wiktionary.org/wiki/File:Fr-coq.ogg
deleted 11y ago
[deleted]
jjgreen 11y ago
It is pronounced "cock" which is (British) English for a male chicken, what an American might call a rooster. Not surprising, as cock is derived from the French _coq_.
- asmodian 11y ago
  In USA, cock is pretty much just about penis. Another one I hear is fag / faggot, which is considered hate speech and grounds for immediate termination. I understand you just want to program. I knew the answer before you responded because I made the deliberate attempt to understand. Twitter gangs won't extend the same courtesy to you when their livelihood depends on stowing outrage over cheap gambits like that. These days in USA non-programmers can easily invoke code of conduct to have careers permanently ruined. Canadian harassment laws now cover disagreeing with females' sensibilities also can get you in jail.
  - mikegerwitz 11y ago
    I upvoted your original question because it is a legitimate one, whether others like it or not. I actually have gotten very few odd looks even from non-programmers when pronouncing "Coq" as "cock" _in the proper context_. "Use Coq" would probably yield a different out-of-context interpretation than "For problem X I think we should consider Coq. It allows ..." I don't think this is much of a problem in practice.

geon 11y ago

Heh. CH2O = formaldehyde

vinceyuan 11y ago

The font size on this page is very small. My eyes hurt when I read it on my non-retina 13-inch Macbook Pro (on low-resolution external monitor, it looks bigger.). Is it because I am not a native English speaker? Do native English speakers get used to this font size? Some websites including Hacker News use very small font size. Reddit's font size is bigger. I created a HN web reader ( http://hackernewsroom.com http://hackernewsroom.com ) with bigger font size (for myself and friends) to read titles and comments easily. But I can't change the font size of the original article. (Have to zoom in the page by pressing cmd+=)

testtest 11y ago
It might be because the font size is defined in the CSS in pixel units, instead of em, which is a point size (DPI dependent). http://www.w3.org/TR/REC-CSS2/syndata.html#length-units http://www.w3.org/TR/REC-CSS2/syndata.html#length-units If you have a problem reading text on the screen, I suggest you use something like Clearly extension that reformats pages with a much more reading-friendly style. You don't have to sign up to use this extension : https://evernote.com/clearly/ https://evernote.com/clearly/ You can also try to print the page into a PDF and read it like that.
- wereHamster 11y ago
  Note that CSS pixels are not the same as physical pixels. Browsers are free to rescale CSS pixel values. Indeed, it's written in the document you linked to: > If the pixel density of the output device is very different from that of a typical computer display, the user agent should rescale pixel values. So actually 12px font should look about the same on all output devices, regardless of their physical DPI. But I agree that 12px is rather small for copy text.
  - Someone 11y ago
    12px font also could become very small in the future, if typical computer displays end up having high dpi. I guess a conforming browser should randomly sample computer displays before deciding how big 1px is. Serious version: I don't think text like that should make it into a standard.

alexbock 11y ago

One issue with this is that the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. The official standards mailing lists for C and C++ are constantly filled with issues regarding inconsistencies in the ISO standards, and for C++ at least people often resort to trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear. It might be a bit better with C, but I once tried to start implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly. There are so many pieces where you are just expected to know what they intend and what inconsistencies can be ignored because you're already familiar with the language that it would be difficult to call any one person's interpretation a formalization of the standard itself.

thinkpad20 11y ago
> the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. Interesting! If the standard is under-specified, then presumably this student must have had to fill in some of the holes themselves, or found a way to represent multiple interpretations simultaneously. > issues regarding inconsistencies in the ISO standards If the standards are inconsistent (in a logical sense), and this formalization is sufficiently complete, it should uncover those inconsistencies since they would amount to type errors in Coq. I wonder if the author had any of those difficulties. > trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear One of the effects a project like this could have is to make this (at least theoretically) unnecessary to do. > implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? I'm not sure what the C standard is but it must be quite a bit smaller. Regardless, it's a PhD thesis so the difficulty of the task isn't a reason not to attempt it :)
- nly 11y ago
  > Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? The language specification itself is only about ~450 pages, the rest is library. It of course inherits all of the insanity of C on top of that (~170 pages of C language spec), which I'd argue brings a disproportionately large share of the pain. Alex's point is that the standard doesn't really begin to give you an idea how hard it is to write an implementation, or make decisions about everything that's unspecified or ambiguous.

sanxiyn 11y ago

Note that this formalization is substantially incomplete: check page 195. CH2O does not formalize variadic function, float, bit field, setjmp/longjmp. All of them are formalized in KCC. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics

deleted 11y ago
[deleted]
- sanxiyn 11y ago
  No, I am referring to PDF page 195.
redsymbol 11y ago
That's true. The immediate-term impact is probably minimal, for the reasons you mention. However, this is a major accomplishment. As this work is built upon, its longer-term impact has the potential to be very significant.
- sanxiyn 11y ago
  I agree it is a major accomplishment. I have doubts about its impact, because I am unsure whether it will be built upon. CH2O's main innovation is C standard (as opposed to C implementation) formalized in general purpose prover (as opposed to custom system). KCC formalized C standard, but not in general purpose prover. CompCert formalized in general purpose prover, but formalized implementation instead of standard. Formalizing in general purpose prover is useful because you can use all of math to prove runtime invariants. But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. For time when you want to prove abstractly to standard, this doesn't seem better than KCC. In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me.
  - baq 11y ago
    it's a phd thesis that advances state of the art. to me it feels you have expectations verging on, please excuse my wording, unreasonable.

JabavuAdams 11y ago

> Surprisingly, correctly describing the set of programs that have undefined behavior in a formal manner is the hardest part of formalizing C. Isn't this undecidable?

obastani 11y ago
I think that statement is referring to simply defining "undefined behavior", not actually determining whether a given program has undefined behavior.
mikeash 11y ago
Yes, but that doesn't mean you can't describe it. The halting problem is undecidable, but it's really easy to describe the set of programs that halt. I just described it right there! That quote is talking about defining the set, not determining whether a program is a member of the set (which is indeed impossible in the general case).

LukeHoersten 11y ago

awesome

rav 11y ago

In a sense, Robbert's thesis can be viewed as a more mathematically stringent (and thus arguably clearer) C11 specification. For instance, page 42 has the following mathematical gem: > The C11 standard defines the usual arithmetic conversions as a binary operation on integer types. This definition is complicated and contains some implicit duplication due to symmetry, which is inconvenient when proving properties. To improve the situation, we show that the usual arithmetic conversion of integer types τ_i and σ_i is a least upper bound τ_i ∪ σ_i in a join semi-lattice.