4 ms·

Compilation: - Meta-tracing, e.g. PyPy. - End-to-end verification of compilers, e.g. CompCert and CakeML. Programming languages: - Mainstreamisation of the

by mafribe 10y ago

Compilation: - Meta-tracing, e.g. PyPy. - End-to-end verification of compilers, e.g. CompCert and CakeML. Programming languages: - Mainstreamisation of the ideas of ML-like languages, e.g. Scala, Rust, Haskell, and the effect these ideas have on legacy languages, e.g. C++, Java 9, C#. - Beginning of use of resource types outside pure research, e.g. affine types in Rust and experimental use of session types. Foundation of mathematics: - Homotopy type theory. - Increasing mainstreamisation of interactive theorem provers, e.g. Isabelle/HOL, Coq, Agda. Program verification: - Increasing ability to have program logics for most programming language constructs. - Increasingly usable automatic theorem provers (SAT and SMT solvers) that just about everything in automated program verification 'compiles' down to.

dorian-graph 10y ago
For someone wanting to begin involving program verification in a practical way to their day-to-day work, do you have any suggestions, resources, or anything?
- mafribe 10y ago
  That depends on your background and your goals. How much do you know about modern testing, abstract interpretation, SAT/SMT solving? In any case, as of Feb 2017, a lot of this technology is not yet economical for non-safety critical mainstream programming. Peter O'Hearn's talk at the Turing Institute https://www.youtube.com/watch?v=lcVx3g3SmmY https://www.youtube.com/watch?v=lcVx3g3SmmY might be of interest.
  - dorian-graph 10y ago
    Very little on abstract interpretation and SAT/SMT solving. I'm effectively starting from 0. I'll go through the talk, thanks! Why isn't it economical yet?
    - munin 10y ago
      Google "certified programming with dependent types", "program logics for certified compilers" and "software foundations class". Also, work through the Dafny tutorials, here: http://rise4fun.com/Dafny/tutorial http://rise4fun.com/Dafny/tutorial There are some ways in which these tools are not economical. There is currently a big gap. On one side of the gap, you have SMT solvers, which have encoded in them decades of institutional knowledge about generating solutions to formula. An SMT solver is filled with tons of "strategies" and "tactics" which are also known has "heuristics" and "hacks" to everyone else. It applies those heuristics, and a few core algorithms, to formula to automatically come up with a solution. This means that the behavior is somewhat unpredictable, sometimes you can have a formula with 60,000 free variables solved in under half a second, sometimes you can have a formula with 10 that takes an hour. It sucks when that's in your type system, because then your compilation speeds become variable. Additionally, it's difficult to debug why compiling something would be slow (and by slow, I mean sometimes it will "time out" because otherwise it would run forever) because you have to trace through your programming language's variables into the solvers variables. If a solver can say "no, this definitely isn't safe" most tools are smart enough to pull the reasoning for "definitively not safe" out into a path through the program that the programmer can study. On the other end of the spectrum are tools like coq and why3. They do very little automatically and require you, the programmer, to specify in painstaking detail why your program is okay. For an example of what I mean by "painstaking" the theorem prover coq could say to you "okay, I know that x = y, and that x and y are natural numbers, but what I don't know is if y = x." You have to tell coq what axiom, from already established axioms, will show that x = y implies y = x. Surely there's room for some compromise, right? Well, this is an active area of research. I am working on projects that try to strike a balance between these two design points, as are many others, but unlike the GP I don't think there's anything to be that excited about yet. There's a lot of problems with existing work and applying it to the real world. Tools that reason about C programs in coq have a very mature set of libraries/theorems to reason about memory and integer arithmetic but the libraries they use to turn C code into coq data structures can't deal with C code constructs like "switch." Tools that do verification at the SMT level are frequently totally new languages, with limited/no interoperability with existing libraries, and selling those in the real world is hard. It's unlikely that any of this will change in the near term because the community of people that care enough about their software reliability is very small and modestly funded. Additionally, making usable developer tools is an orthogonal skill from doing original research, and as a researcher, I both am not rewarded for making usable developer tools, and think that making usable developer tools is much, much harder than doing original research.
  - petra 10y ago
    >> not yet economical Don't know much about it, but verum.com claims 50% reduction in development costs.
bem94 10y ago
I work in CPU design. So I'd add that the tools for formally verifying CPUs have come a very long way in the last two years, and the next two years look like they will be very exciting indeed.
- kbradero 10y ago
  wow ! what tools are you guys using ?, do you have the same for microcode ? this is really interesting !
- kevinnk 10y ago
  I'd also like to hear more about what tools you're using/looking forward to.
- mafribe 10y ago
  There is a big overlap in prover theory. HOL Light comes from Intelite John Harrison. I don't know much about CPUs, but I suspect that one of the core problems of software verification, the absence of a useful specification, isn't much of an issue with hardware.
ecesena 10y ago
There's a new project to implement TLS in python [1] with the idea to have secure and verifiable code, but so far (to my knowledge) there's no formal tool involved in the verifiability aspect -- the approach is mostly around keeping the implementation as RFC-compliant as possible. I'd be really interested in applying any of these techniques to a full TLS implementation. [1] https://github.com/pyca/tls https://github.com/pyca/tls
- mafribe 10y ago
  I recommend to look at Cedric Fournet's group [1]. They have (or are close to having) a performant networking stack that's fully verified, e.g. [2]. [1] http://research.microsoft.com/en-us/um/people/fournet http://research.microsoft.com/en-us/um/people/fournet [2] K. Bhargavan et al, Implementing TLS with Verified Cryptographic Security. http://research.microsoft.com/en-us/um/people/fournet/papers/implementing-tls-with-verified-cryptographic-security-sp13.pdf http://research.microsoft.com/en-us/um/people/fournet/papers...
adamnemecek 10y ago
> Homotopy type theory. Can you talk more about this? I even got THE book on this (haven't really read it yet though) and like I think I get the rough ideas but I'd be curious to hear what HTT means to you (lol).
- maxiepoo 10y ago
  Not the OP, but the cool thing about HoTT to a user of proof assistants is that it makes working with "quotients" easier. I put quotients in parentheses because really HoTT is about generalizing the idea of a quotient type. Quotients of sets/algebras are one of the core tools of mathematics and old school type theory doesn't have them so you have to manually keep around equivalence relations and prove over and over again that you respect the relations. In HoTT, there is an extension of inductive types that allows you to, not just have constructors, but also to impose "equalities" so these generalized "quotients" really have first-class status in the language. As far as "exciting developments" in HoTT, the big one right now is Cubical Type Theory [1], which is the first implementation of the new ideas of HoTT where Higher inductive types and the univalence axiom "compute" which means that the proof assistant can do more work for you when you use those features. I just saw a talk about it and from talking to people about it, this means that it won't be too long (< 5 years I predict) before we have this stuff implemented in Agda and/or Coq. Finally, I just want to say to people that are scared off or annoyed by all of the abstract talk about "homotopies" and "cubes", you have to understand that this is very new research and we don't yet know the best ways to use and explain these concepts. I certainly think that people will be able to use this stuff without having to learn anything about homotopy theory, though the intuition will probably help. [1] https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt
- mafribe 10y ago
  HoTT means a lot to me (lol) HoTT brought dependent types and interactive theorem proving to the masses. Before HoTT, the number of researchers working seriously on dependent type theory was probably < 20. This has now changed, and the field is developing at a much more rapid pace than before.

by mafribe 10y ago

dorian-graph 10y ago

For someone wanting to begin involving program verification in a practical way to their day-to-day work, do you have any suggestions, resources, or anything?

mafribe 10y ago
That depends on your background and your goals. How much do you know about modern testing, abstract interpretation, SAT/SMT solving? In any case, as of Feb 2017, a lot of this technology is not yet economical for non-safety critical mainstream programming. Peter O'Hearn's talk at the Turing Institute https://www.youtube.com/watch?v=lcVx3g3SmmY https://www.youtube.com/watch?v=lcVx3g3SmmY might be of interest.
- dorian-graph 10y ago
  Very little on abstract interpretation and SAT/SMT solving. I'm effectively starting from 0. I'll go through the talk, thanks! Why isn't it economical yet?
  - munin 10y ago
    Google "certified programming with dependent types", "program logics for certified compilers" and "software foundations class". Also, work through the Dafny tutorials, here: http://rise4fun.com/Dafny/tutorial http://rise4fun.com/Dafny/tutorial There are some ways in which these tools are not economical. There is currently a big gap. On one side of the gap, you have SMT solvers, which have encoded in them decades of institutional knowledge about generating solutions to formula. An SMT solver is filled with tons of "strategies" and "tactics" which are also known has "heuristics" and "hacks" to everyone else. It applies those heuristics, and a few core algorithms, to formula to automatically come up with a solution. This means that the behavior is somewhat unpredictable, sometimes you can have a formula with 60,000 free variables solved in under half a second, sometimes you can have a formula with 10 that takes an hour. It sucks when that's in your type system, because then your compilation speeds become variable. Additionally, it's difficult to debug why compiling something would be slow (and by slow, I mean sometimes it will "time out" because otherwise it would run forever) because you have to trace through your programming language's variables into the solvers variables. If a solver can say "no, this definitely isn't safe" most tools are smart enough to pull the reasoning for "definitively not safe" out into a path through the program that the programmer can study. On the other end of the spectrum are tools like coq and why3. They do very little automatically and require you, the programmer, to specify in painstaking detail why your program is okay. For an example of what I mean by "painstaking" the theorem prover coq could say to you "okay, I know that x = y, and that x and y are natural numbers, but what I don't know is if y = x." You have to tell coq what axiom, from already established axioms, will show that x = y implies y = x. Surely there's room for some compromise, right? Well, this is an active area of research. I am working on projects that try to strike a balance between these two design points, as are many others, but unlike the GP I don't think there's anything to be that excited about yet. There's a lot of problems with existing work and applying it to the real world. Tools that reason about C programs in coq have a very mature set of libraries/theorems to reason about memory and integer arithmetic but the libraries they use to turn C code into coq data structures can't deal with C code constructs like "switch." Tools that do verification at the SMT level are frequently totally new languages, with limited/no interoperability with existing libraries, and selling those in the real world is hard. It's unlikely that any of this will change in the near term because the community of people that care enough about their software reliability is very small and modestly funded. Additionally, making usable developer tools is an orthogonal skill from doing original research, and as a researcher, I both am not rewarded for making usable developer tools, and think that making usable developer tools is much, much harder than doing original research.
- petra 10y ago
  >> not yet economical Don't know much about it, but verum.com claims 50% reduction in development costs.

bem94 10y ago

I work in CPU design. So I'd add that the tools for formally verifying CPUs have come a very long way in the last two years, and the next two years look like they will be very exciting indeed.

kbradero 10y ago
wow ! what tools are you guys using ?, do you have the same for microcode ? this is really interesting !
kevinnk 10y ago
I'd also like to hear more about what tools you're using/looking forward to.
mafribe 10y ago
There is a big overlap in prover theory. HOL Light comes from Intelite John Harrison. I don't know much about CPUs, but I suspect that one of the core problems of software verification, the absence of a useful specification, isn't much of an issue with hardware.

ecesena 10y ago

There's a new project to implement TLS in python [1] with the idea to have secure and verifiable code, but so far (to my knowledge) there's no formal tool involved in the verifiability aspect -- the approach is mostly around keeping the implementation as RFC-compliant as possible. I'd be really interested in applying any of these techniques to a full TLS implementation. [1] https://github.com/pyca/tls https://github.com/pyca/tls

mafribe 10y ago
I recommend to look at Cedric Fournet's group [1]. They have (or are close to having) a performant networking stack that's fully verified, e.g. [2]. [1] http://research.microsoft.com/en-us/um/people/fournet http://research.microsoft.com/en-us/um/people/fournet [2] K. Bhargavan et al, Implementing TLS with Verified Cryptographic Security. http://research.microsoft.com/en-us/um/people/fournet/papers/implementing-tls-with-verified-cryptographic-security-sp13.pdf http://research.microsoft.com/en-us/um/people/fournet/papers...

adamnemecek 10y ago

> Homotopy type theory. Can you talk more about this? I even got THE book on this (haven't really read it yet though) and like I think I get the rough ideas but I'd be curious to hear what HTT means to you (lol).

maxiepoo 10y ago
Not the OP, but the cool thing about HoTT to a user of proof assistants is that it makes working with "quotients" easier. I put quotients in parentheses because really HoTT is about generalizing the idea of a quotient type. Quotients of sets/algebras are one of the core tools of mathematics and old school type theory doesn't have them so you have to manually keep around equivalence relations and prove over and over again that you respect the relations. In HoTT, there is an extension of inductive types that allows you to, not just have constructors, but also to impose "equalities" so these generalized "quotients" really have first-class status in the language. As far as "exciting developments" in HoTT, the big one right now is Cubical Type Theory [1], which is the first implementation of the new ideas of HoTT where Higher inductive types and the univalence axiom "compute" which means that the proof assistant can do more work for you when you use those features. I just saw a talk about it and from talking to people about it, this means that it won't be too long (< 5 years I predict) before we have this stuff implemented in Agda and/or Coq. Finally, I just want to say to people that are scared off or annoyed by all of the abstract talk about "homotopies" and "cubes", you have to understand that this is very new research and we don't yet know the best ways to use and explain these concepts. I certainly think that people will be able to use this stuff without having to learn anything about homotopy theory, though the intuition will probably help. [1] https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt
mafribe 10y ago
HoTT means a lot to me (lol) HoTT brought dependent types and interactive theorem proving to the masses. Before HoTT, the number of researchers working seriously on dependent type theory was probably < 20. This has now changed, and the field is developing at a much more rapid pace than before.