8 ms·

Interview with Xavier Leroy

151 points by panic 9y ago

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.
systems 9y ago
Might be important to mention (in the title) that Xavier Leroy, is the lead OCaml developer Not everyone might be familiar with the name
- seanmcdirmid 9y ago
  On the other hand, anyone in PL academics should be familiar with his name.
  - d215 9y ago
    On the other hand there are scores of people not in PL academics that are interested in OCaml. People that might have heard of Reason for example.
cdancette 9y ago
I learned caml in France during my studies, as stated in the article. But it's far from being the language "everyone teaches in french schools". It's only taught in a specific specialization (computer science) before engineering school, so that's about 1000-2000 students every year. I think the most taught languages are still Java and python by far. I really liked this language though, it's very elegant and concise to write cs-related algorithms, and to do symbolic manipulation.
- gaius 9y ago
  I learned caml in France during my studies, as stated in the article. But it's far from being the language "everyone teaches in french schools". It's only taught in a specific specialization (computer science) before engineering school, so that's about 1000-2000 students every year. I never understood this. OCaml is a world-class language, if the French threw the weight of their education system behind it, mandated it as the language for government IT work to build a critical mass, they would have a killer advantage. But I guess the demise of Le Minitel has made them afraid of home-grown technologies, it is a huge missed opportunity. It's the same as if the British government had had the foresight to back the Acorn ecosystem. We would be 15-20 years ahead of where we are now. An Archimedes on every desktop...
  - emmelaich 9y ago
    Maybe they're once bitten (by Minitel) twice shy.
    - angry_octet 9y ago
      Why do you say Minitel was so bad? From an outside perspective it is brilliant. It was late '90s before the internet had anything like the penetration of Minitel. Arguably, the French should have continued inovating Minitel. Re-written the terminal software in OCaml.
  - bsaul 9y ago
    Small personal story as a former french cs student : I remember my thought when i was taught oCaml : we had to recode ocaml type inference, in ocaml. The teacher was really satisfied in the end , saying things like « that’s good ! Now you see, type inference is like a theorem proof ». It took me ten years to understand what i did this day, and what my teacher meant. When i was a student, i wanted to program videogames ( like many cs student i suppose), so all this research and very theoretical concerns were very very remote from my interest. Ocaml was a weird thing that had very little to do with my future everyday job. And now i start to look at F# for web development, thinking that the whole stuff is just beautiful.
gwenzek 9y ago
> I also wanted to talk about how OCaml came about. Did you expect it to be the language everyone taught in French schools? Since 2012 most students learn Python, which is a shame IMHO. Learning OCaml will make you a better programmer for the rest of your life, while learning Python doesn't teach you much about programming.
- wiz21c 9y ago
  Yep, Python made me productive, Java made me collaborative but only Scheme made me understand. (In fact it's another way around : I learned basic at 10, assembly at 14, pascal at 16 then I learned Scheme (continuations, tunks, parallelism, etc) at 22 at university and realized "now I understand what I've been doing the last 10 years)
- B1FF_PSUVM 9y ago
  > while learning Python doesn't teach you much about programming. I once tried to teach Python to biologists. It's also enlightening - many people don't "get" programming of any kind (except perhaps spreadsheets ;-). If you already get it, then of course a different paradigm will shine new light.

151 points by panic 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.

systems 9y ago

Might be important to mention (in the title) that Xavier Leroy, is the lead OCaml developer Not everyone might be familiar with the name

seanmcdirmid 9y ago
On the other hand, anyone in PL academics should be familiar with his name.
- d215 9y ago
  On the other hand there are scores of people not in PL academics that are interested in OCaml. People that might have heard of Reason for example.

cdancette 9y ago

I learned caml in France during my studies, as stated in the article. But it's far from being the language "everyone teaches in french schools". It's only taught in a specific specialization (computer science) before engineering school, so that's about 1000-2000 students every year. I think the most taught languages are still Java and python by far. I really liked this language though, it's very elegant and concise to write cs-related algorithms, and to do symbolic manipulation.

gaius 9y ago
I learned caml in France during my studies, as stated in the article. But it's far from being the language "everyone teaches in french schools". It's only taught in a specific specialization (computer science) before engineering school, so that's about 1000-2000 students every year. I never understood this. OCaml is a world-class language, if the French threw the weight of their education system behind it, mandated it as the language for government IT work to build a critical mass, they would have a killer advantage. But I guess the demise of Le Minitel has made them afraid of home-grown technologies, it is a huge missed opportunity. It's the same as if the British government had had the foresight to back the Acorn ecosystem. We would be 15-20 years ahead of where we are now. An Archimedes on every desktop...
- emmelaich 9y ago
  Maybe they're once bitten (by Minitel) twice shy.
  - angry_octet 9y ago
    Why do you say Minitel was so bad? From an outside perspective it is brilliant. It was late '90s before the internet had anything like the penetration of Minitel. Arguably, the French should have continued inovating Minitel. Re-written the terminal software in OCaml.
- bsaul 9y ago
  Small personal story as a former french cs student : I remember my thought when i was taught oCaml : we had to recode ocaml type inference, in ocaml. The teacher was really satisfied in the end , saying things like « that’s good ! Now you see, type inference is like a theorem proof ». It took me ten years to understand what i did this day, and what my teacher meant. When i was a student, i wanted to program videogames ( like many cs student i suppose), so all this research and very theoretical concerns were very very remote from my interest. Ocaml was a weird thing that had very little to do with my future everyday job. And now i start to look at F# for web development, thinking that the whole stuff is just beautiful.

gwenzek 9y ago

> I also wanted to talk about how OCaml came about. Did you expect it to be the language everyone taught in French schools? Since 2012 most students learn Python, which is a shame IMHO. Learning OCaml will make you a better programmer for the rest of your life, while learning Python doesn't teach you much about programming.

wiz21c 9y ago
Yep, Python made me productive, Java made me collaborative but only Scheme made me understand. (In fact it's another way around : I learned basic at 10, assembly at 14, pascal at 16 then I learned Scheme (continuations, tunks, parallelism, etc) at 22 at university and realized "now I understand what I've been doing the last 10 years)
B1FF_PSUVM 9y ago
> while learning Python doesn't teach you much about programming. I once tried to teach Python to biologists. It's also enlightening - many people don't "get" programming of any kind (except perhaps spreadsheets ;-). If you already get it, then of course a different paradigm will shine new light.