4 ms·

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 che

by 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?

by csb6 7y ago

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?