8 ms·

Nice interview. What a tremendous achievement to formally prove the correctness of a C compiler! It boggles my mind why more people are not involved in this dir

by 110011 9y ago

Nice interview. What a tremendous achievement to formally prove the correctness of a C compiler! It boggles my mind why more people are not involved in this direction. I hope to live to see the day when lots of commercial software will be written with formal proofs and zero tests. It may just be that we don't have the right tools at this point. If theorem provers could figure out details for themselves for the most part and the programmer has to only specify a few key invariants and rough sketches of the hypotheses and the end guarantees then I cannot begin to imagine how much more productive programming can become.

ihm 9y ago
I think it is an exciting time for functional programming and formal methods: they seem to have found something of a home in the recent cryptocurrency boom, where people are recognizing that high-assurance really matters lest you lose millions of dollars. Why people don't seem to worry as much about self-driving cars boggles the mind. One hopes the loss of human life would be as concerning as the loss of money. I think the issue is partly technological. As Leroy says, formal methods for certifying machine learning-produced models are pretty undeveloped whereas cryptocurrency protocols are 'traditional', 'algorithmic' programs and so more amenable to analysis with existing verification tools. I also think it is partly cultural in that machine learning practitioners seem often to be less aware of formal methods and the possibility of verifying software.
- haskellandchill 9y ago
  I don’t see many options career wise however, I invested heavily in formal methods but I think it’s time for me to pivot to machine learning and data science to have higher paying job opportunities in NYC. I still believe it will have a major moment in the future and Proof Engineer will be a thing.
  - auggierose 9y ago
    Proof engineer is a thing. It's just that there are only a handful of them :)
- bagnalla 9y ago
  Verification of machine learning models, especially w.r.t. robustness to so-called "adversarial examples" [1], is a major research topic at the moment. There are certainly people worrying about it in the machine learning community, but it appears to be a very difficult problem. [1] https://arxiv.org/abs/1312.6199 https://arxiv.org/abs/1312.6199
kazinator 9y ago
> It boggles my mind why more people are not involved in this direction. Because only a vanishingly rare amount of the incorrectness in compiled C programs comes from a bug in the compiler. Also, some code coaxes a desired behavior out of the object code while bending the rules of the language. The compiler being proven over correct code (i.e. free of any undefined behaviors) is useless in that situation, unless the prover actually works with an extended language definition (specific to that compiler) which defines those behaviors.
- angry_octet 9y ago
  Well, it does define a subset of C... Anything in that subset will run as specified in a correct physical machine. So I don't get your point? Are you saying that a verified compiler is useless if you write buggy software? Because that isn't really a criticism. Have you read anything about CompCert C or Coq?
  - 110011 9y ago
    What OP is saying is if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. And this does account for the vast majority of bugs (programmer error compared to compiler error).
    - catnaroek 9y ago
      > if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. This is not true. It means that you can safely omit the compiler writer from the list of people to burn at the stake.
      - kazinator 9y ago
        > It means that you can safely omit the compiler writer from the list of people to burn at the stake. Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too. Say we have an open source distro full of programs, and a compiler change breaks some program that hasn't been touched in years so that it misbehaves in situations where old builds of that program do not. This means the compiler writers aren't testing with a full distro, and possibly that they don't care. "We can do anything we want within the limits set out by the ISO language spec, and that spec alone; let the downstream consumers sort out whatever happens."
dpandya 9y ago
> It may just be that we don't have the right tools at this point. The real reason is that the solution to this problem isn't valuable to most people that have the resources to pay for a solution. Most bugs aren't caused by issues in the C compiler. There are many technically challenging, interesting problems that face a similar predicament. The people who solve them will generally find some way to tie them back to reality.

by 110011 9y ago

ihm 9y ago

I think it is an exciting time for functional programming and formal methods: they seem to have found something of a home in the recent cryptocurrency boom, where people are recognizing that high-assurance really matters lest you lose millions of dollars. Why people don't seem to worry as much about self-driving cars boggles the mind. One hopes the loss of human life would be as concerning as the loss of money. I think the issue is partly technological. As Leroy says, formal methods for certifying machine learning-produced models are pretty undeveloped whereas cryptocurrency protocols are 'traditional', 'algorithmic' programs and so more amenable to analysis with existing verification tools. I also think it is partly cultural in that machine learning practitioners seem often to be less aware of formal methods and the possibility of verifying software.

haskellandchill 9y ago
I don’t see many options career wise however, I invested heavily in formal methods but I think it’s time for me to pivot to machine learning and data science to have higher paying job opportunities in NYC. I still believe it will have a major moment in the future and Proof Engineer will be a thing.
- auggierose 9y ago
  Proof engineer is a thing. It's just that there are only a handful of them :)
bagnalla 9y ago
Verification of machine learning models, especially w.r.t. robustness to so-called "adversarial examples" [1], is a major research topic at the moment. There are certainly people worrying about it in the machine learning community, but it appears to be a very difficult problem. [1] https://arxiv.org/abs/1312.6199 https://arxiv.org/abs/1312.6199

kazinator 9y ago

> It boggles my mind why more people are not involved in this direction. Because only a vanishingly rare amount of the incorrectness in compiled C programs comes from a bug in the compiler. Also, some code coaxes a desired behavior out of the object code while bending the rules of the language. The compiler being proven over correct code (i.e. free of any undefined behaviors) is useless in that situation, unless the prover actually works with an extended language definition (specific to that compiler) which defines those behaviors.

angry_octet 9y ago
Well, it does define a subset of C... Anything in that subset will run as specified in a correct physical machine. So I don't get your point? Are you saying that a verified compiler is useless if you write buggy software? Because that isn't really a criticism. Have you read anything about CompCert C or Coq?
- 110011 9y ago
  What OP is saying is if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. And this does account for the vast majority of bugs (programmer error compared to compiler error).
  - catnaroek 9y ago
    > if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. This is not true. It means that you can safely omit the compiler writer from the list of people to burn at the stake.
    - kazinator 9y ago
      > It means that you can safely omit the compiler writer from the list of people to burn at the stake. Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too. Say we have an open source distro full of programs, and a compiler change breaks some program that hasn't been touched in years so that it misbehaves in situations where old builds of that program do not. This means the compiler writers aren't testing with a full distro, and possibly that they don't care. "We can do anything we want within the limits set out by the ISO language spec, and that spec alone; let the downstream consumers sort out whatever happens."

dpandya 9y ago

> It may just be that we don't have the right tools at this point. The real reason is that the solution to this problem isn't valuable to most people that have the resources to pay for a solution. Most bugs aren't caused by issues in the C compiler. There are many technically challenging, interesting problems that face a similar predicament. The people who solve them will generally find some way to tie them back to reality.