9 ms·

That is very inaccurate. TLA+ is normally used for things that are much bigger than Coq could feasibly be used for at all. They're aimed for programs of complet

by pron 5y ago

That is very inaccurate. TLA+ is normally used for things that are much bigger than Coq could feasibly be used for at all. They're aimed for programs of completely different orders of magnitude. TLA+ is commonly used by engineers to specify and check systems or components with tens of thousands or hundreds of thousands of lines over, say, a couple of weeks. Coq and other things that are more aimed at end-to-end verification, all the way to code, have only ever been used on programs or components less than 10KLOC, and even then required teams of world-experts working for years.

hansvm 5y ago
> That is very inaccurate. Nah, we just didn't talk about the downsides you're mentioning. The fact that there are downsides doesn't make everything else false. > 10KLOC ~100KSLOC (e.g., CompCert) > and even then required teams of world-experts working for years Definitely. A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project, but it's pretty hard to use right now.
- kaba0 5y ago
  As far as I know formal verification doesn’t necessarily give way for much parallelism, and the halting problem will not become obsolete, and the latter is a lower bound on many interesting properties. So unless there is a radically new way to serial computations, that is orders of magnitude faster, I doubt much would change. CPUs are already quite at the limit with super-scalar architectures.
  - jerome-jh 5y ago
    Of course verification in its full generality is a dead end. However expressing an algorithm in a sound logical system, and proving properties of the algorithm is quite fruitful. That's the approach taken by Coq and probably others. Most of the time the prover still needs some guidance from the user though.
- pron 5y ago
  > The fact that there are downsides doesn't make everything else false. When we say something can be done but mean that it can be done only by a select few, at great effort, and at a scale that's orders of magnitude smaller than what that "thing" normally is, then the meaning of "can" is misleading. > ~100KSLOC (e.g., CompCert) The total proofs may come out to that, but it corresponds to a ~10KLOC program (without proofs). > A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project The problem is that the gap between programs that can be verified end-to-end with the semi-manual deductive proof technique used by Coq and other proof assistant and the typical software has been gradually growing, as the scale of software has grown faster than the scale of effective deductive-proof techniques. Today we can verify smaller programs relative to the average program size using such techniques than we could twenty and thirty years ago (although that's not to say that our ability to use that particular technique for small but critical components hasn't improved, and that is where that technique is hoped to be more widely applied). Which is why many in the formal verification space are looking in other directions when it comes to verifying the actual code, mostly methods that forgo soundness, like concolic testing and its descendants.

by pron 5y ago

hansvm 5y ago

> That is very inaccurate. Nah, we just didn't talk about the downsides you're mentioning. The fact that there are downsides doesn't make everything else false. > 10KLOC ~100KSLOC (e.g., CompCert) > and even then required teams of world-experts working for years Definitely. A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project, but it's pretty hard to use right now.

kaba0 5y ago
As far as I know formal verification doesn’t necessarily give way for much parallelism, and the halting problem will not become obsolete, and the latter is a lower bound on many interesting properties. So unless there is a radically new way to serial computations, that is orders of magnitude faster, I doubt much would change. CPUs are already quite at the limit with super-scalar architectures.
- jerome-jh 5y ago
  Of course verification in its full generality is a dead end. However expressing an algorithm in a sound logical system, and proving properties of the algorithm is quite fruitful. That's the approach taken by Coq and probably others. Most of the time the prover still needs some guidance from the user though.
pron 5y ago
> The fact that there are downsides doesn't make everything else false. When we say something can be done but mean that it can be done only by a select few, at great effort, and at a scale that's orders of magnitude smaller than what that "thing" normally is, then the meaning of "can" is misleading. > ~100KSLOC (e.g., CompCert) The total proofs may come out to that, but it corresponds to a ~10KLOC program (without proofs). > A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project The problem is that the gap between programs that can be verified end-to-end with the semi-manual deductive proof technique used by Coq and other proof assistant and the typical software has been gradually growing, as the scale of software has grown faster than the scale of effective deductive-proof techniques. Today we can verify smaller programs relative to the average program size using such techniques than we could twenty and thirty years ago (although that's not to say that our ability to use that particular technique for small but critical components hasn't improved, and that is where that technique is hoped to be more widely applied). Which is why many in the formal verification space are looking in other directions when it comes to verifying the actual code, mostly methods that forgo soundness, like concolic testing and its descendants.