6 ms·

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific t

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS heap, and then we have system objects involved in basic I/O that aren't necessarily tied to a particular JS isolate and are not garbage collected, but are often tied to specific OS threads. JS objects and system objects are allowed to own instances of each other, but the ownership must be handled in a special way. E.g., when a system object holds a reference to a JS object, the destructor must ensure the JS isolate lock is held before releasing that reference. Conversely when a JS object holds ownership of a system object, and the JS object is garbage collected, we need to queue the system object's destructor to run in the thread where it was created. Conceptually, it ought to be easy to write rules where each type is declared as being a system type or a JS type, and then the compiler could trivially enforce that the correct sort of references are used between them. But, the problem is very specific to our codebase, so it would make no sense to bake into the language. I think the next big thing for C++ should be adding ways to define custom code-checking rules like this. It would allow C++ to become a safe language and would fit perfectly with C++'s culture of being ridiculously overcomplicated. ;)

csb6 7y ago
I really like this idea. I’ve been messing around with the z3 theorem prover, and while I don’t think there’s an easy way to integrate it to do compile-time checks, I made a little wrapper class that lets you add assertions which are checked for satisfiability at the end of a function’s scope. But it’s all at runtime, so it’s more like a more advanced assert() than anything like Jai or Rust has. I think SMT solvers are criminally under used and have a lot of potential to help solve some of the issues in a way that still allows rapid iteration at first and then incremental safety checks to be added on later.
- glangdale 7y ago
  I like this idea too, but bear in mind that the world of SMT in general (Z3 not an exception) seems to have a lot of cosmetically-similar formulations some of which are trivial and some of which will take forever to solve. The honeymoon with SMT is often brief. You've gotten through the whole 'hooray, now I can nuke Sudoko and those "Mr Brown lives on the same street as the baker, who has a white house" problems' and surely all the world's problems will fall to my awesome new abilities. You then put some basic quantifier problems into Z3 or whatever and watch the prompt go away, apparently permanently. I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research.
  - akgvn 7y ago
    > I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research. Agreed. I've been doing some research to create an SAT Solver and found surprisingly low amount of learning material. I'd love some recommendations from HN crowd.
    - taejo 7y ago
      I learned a good foundation of how SAT solvers work in this course: http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ws17/readings.html http://resources.mpi-inf.mpg.de/departments/rg1/teaching/aut... Lecture notes are there; exercises are available in the linked earlier instances of the course.
  - mmoskal 7y ago
    I wrote a paper on this a few years ago http://moskal.me/pdf/prtrig.pdf http://moskal.me/pdf/prtrig.pdf though indeed getting the quantifiers to verify is more art than science...
- docandrew 7y ago
  You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, including Z3 and CVC4. If you run into something that SMT can't figure out in a reasonable time-frame, you can use Coq to manually-prove your theorems too. Languages like SPARK and Frama C generate Why3ML as an intermediate output that then gets transformed to run against whatever solvers are available during the verification phase of development. Since the verification/proof phase is separate from compilation, you can write your code with fewer checks initially, and then add conditions as you go to prove functional correctness. I'd be surprised if C++ is ever touted seriously as a language suited for formal verification. I think the language just has too many corners and escape hatches to be able to nail down its semantics in a way that automated provers can handle. Having said that though, I'm pretty sure the MSVC Driver Verifier tool uses an SMT solver to try and prove the absence of certain types of errors, so who knows?
Polyisoprene 7y ago
Would dependent types help in this case? Add the reference type when creating the type and then you could have the compiler check that the contract holds.
- kentonv 7y ago
  It might be expressible with dependent types. I think what I'm suggesting ought to be able to express a superset of dependent types. I think a lot of type theory tries too hard to have certain "desirable" properties, like being decidable (that is, type checking will always complete in finite time). IMO it's fine if there are cases that will go into an infinite loop, as long as the developer has tools for debugging and fixing them. After all, we rarely use programming languages where the actual programs aren't allowed to loop -- such languages exist, but they are far too restrictive to be useful for most purposes. Maybe what I want is not even a theorem prover, but just a way to write little scripts that execute in an imperative fashion, which can iterate over the code and look for errors. Why does it have to be a fancy logic language that only academics understand?
  - Dontrememberit 7y ago
    Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether) That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".
    - kentonv 7y ago
      Sorry, I don't understand. Does this non-terminating function run at compile time or at runtime? If it runs at compile time, and it doesn't terminate, then presumably no executable is generated? That's good enough for me. Or are you describing a function that checks some property at runtime, which the type system then depends on afterwards? But if that function never returns, then the subsequent code that depends on the property it was checking won't ever execute. So a false thing is only proven true in code that never executes. That seems fine to me. (Also note that as a practical matter I mostly don't care if it's possible for a developer to maliciously trick the type system. I only care about catching accidental errors. Relying on a complex type checker for sandboxing of malicious code seems too risky.)
ausimian 7y ago
VCC[1] was a substantial piece of research from MSR aimed at supporting the verification of C (not C++) via a theorem prover. However, it appears in a study[2] of its application to parts of the Hyper-V code-base, there were some practical difficulties relating to proving performance in the developer workflow. Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3]. [1] https://github.com/microsoft/vcc https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny
- mmoskal 7y ago
  There are also efforts at ETH to verify Rust using SMT solvers using methods similar to VCC and Dafny, see https://www.pm.inf.ethz.ch/research/prusti.html https://www.pm.inf.ethz.ch/research/prusti.html Adding verification once you have code is generally more difficult, though in case of VCC it was helpful to have a large example code base to make sure the tool would cover the major patterns, especially relating to concurrency primitives.
7thaccount 7y ago
I think Ada + Spark has something along these lines. https://www.adacore.com/about-spark https://www.adacore.com/about-spark
Dontrememberit 7y ago
> I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. Did you take a look at ATS?
- kentonv 7y ago
  I realize there are obscure programming languages that do this stuff, but I need it in C++.
touisteur 7y ago
Wouldn't Frama-C and some of its plugins do this job? I've seen (I think?) Airbus (working with Atos?) people write custom Frama-C plug-ins to implement some static analysis & proof on their code, with great success.
ryuukk_ 7y ago
the next big thing for C++: - reduce compile time by at least 100000000000000000000x - shrink stl by at least 100000000000000000000000000x

csb6 7y ago

I really like this idea. I’ve been messing around with the z3 theorem prover, and while I don’t think there’s an easy way to integrate it to do compile-time checks, I made a little wrapper class that lets you add assertions which are checked for satisfiability at the end of a function’s scope. But it’s all at runtime, so it’s more like a more advanced assert() than anything like Jai or Rust has. I think SMT solvers are criminally under used and have a lot of potential to help solve some of the issues in a way that still allows rapid iteration at first and then incremental safety checks to be added on later.

glangdale 7y ago
I like this idea too, but bear in mind that the world of SMT in general (Z3 not an exception) seems to have a lot of cosmetically-similar formulations some of which are trivial and some of which will take forever to solve. The honeymoon with SMT is often brief. You've gotten through the whole 'hooray, now I can nuke Sudoko and those "Mr Brown lives on the same street as the baker, who has a white house" problems' and surely all the world's problems will fall to my awesome new abilities. You then put some basic quantifier problems into Z3 or whatever and watch the prompt go away, apparently permanently. I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research.
- akgvn 7y ago
  > I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research. Agreed. I've been doing some research to create an SAT Solver and found surprisingly low amount of learning material. I'd love some recommendations from HN crowd.
  - taejo 7y ago
    I learned a good foundation of how SAT solvers work in this course: http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ws17/readings.html http://resources.mpi-inf.mpg.de/departments/rg1/teaching/aut... Lecture notes are there; exercises are available in the linked earlier instances of the course.
- mmoskal 7y ago
  I wrote a paper on this a few years ago http://moskal.me/pdf/prtrig.pdf http://moskal.me/pdf/prtrig.pdf though indeed getting the quantifiers to verify is more art than science...
docandrew 7y ago
You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, including Z3 and CVC4. If you run into something that SMT can't figure out in a reasonable time-frame, you can use Coq to manually-prove your theorems too. Languages like SPARK and Frama C generate Why3ML as an intermediate output that then gets transformed to run against whatever solvers are available during the verification phase of development. Since the verification/proof phase is separate from compilation, you can write your code with fewer checks initially, and then add conditions as you go to prove functional correctness. I'd be surprised if C++ is ever touted seriously as a language suited for formal verification. I think the language just has too many corners and escape hatches to be able to nail down its semantics in a way that automated provers can handle. Having said that though, I'm pretty sure the MSVC Driver Verifier tool uses an SMT solver to try and prove the absence of certain types of errors, so who knows?

Polyisoprene 7y ago

Would dependent types help in this case? Add the reference type when creating the type and then you could have the compiler check that the contract holds.

kentonv 7y ago
It might be expressible with dependent types. I think what I'm suggesting ought to be able to express a superset of dependent types. I think a lot of type theory tries too hard to have certain "desirable" properties, like being decidable (that is, type checking will always complete in finite time). IMO it's fine if there are cases that will go into an infinite loop, as long as the developer has tools for debugging and fixing them. After all, we rarely use programming languages where the actual programs aren't allowed to loop -- such languages exist, but they are far too restrictive to be useful for most purposes. Maybe what I want is not even a theorem prover, but just a way to write little scripts that execute in an imperative fashion, which can iterate over the code and look for errors. Why does it have to be a fancy logic language that only academics understand?
- Dontrememberit 7y ago
  Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether) That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".
  - kentonv 7y ago
    Sorry, I don't understand. Does this non-terminating function run at compile time or at runtime? If it runs at compile time, and it doesn't terminate, then presumably no executable is generated? That's good enough for me. Or are you describing a function that checks some property at runtime, which the type system then depends on afterwards? But if that function never returns, then the subsequent code that depends on the property it was checking won't ever execute. So a false thing is only proven true in code that never executes. That seems fine to me. (Also note that as a practical matter I mostly don't care if it's possible for a developer to maliciously trick the type system. I only care about catching accidental errors. Relying on a complex type checker for sandboxing of malicious code seems too risky.)

ausimian 7y ago

VCC[1] was a substantial piece of research from MSR aimed at supporting the verification of C (not C++) via a theorem prover. However, it appears in a study[2] of its application to parts of the Hyper-V code-base, there were some practical difficulties relating to proving performance in the developer workflow. Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3]. [1] https://github.com/microsoft/vcc https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny

mmoskal 7y ago
There are also efforts at ETH to verify Rust using SMT solvers using methods similar to VCC and Dafny, see https://www.pm.inf.ethz.ch/research/prusti.html https://www.pm.inf.ethz.ch/research/prusti.html Adding verification once you have code is generally more difficult, though in case of VCC it was helpful to have a large example code base to make sure the tool would cover the major patterns, especially relating to concurrency primitives.

7thaccount 7y ago

I think Ada + Spark has something along these lines. https://www.adacore.com/about-spark https://www.adacore.com/about-spark

Dontrememberit 7y ago

> I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. Did you take a look at ATS?

kentonv 7y ago
I realize there are obscure programming languages that do this stuff, but I need it in C++.

touisteur 7y ago

Wouldn't Frama-C and some of its plugins do this job? I've seen (I think?) Airbus (working with Atos?) people write custom Frama-C plug-ins to implement some static analysis & proof on their code, with great success.

ryuukk_ 7y ago

the next big thing for C++: - reduce compile time by at least 100000000000000000000x - shrink stl by at least 100000000000000000000000000x