4 ms·

The comment about the cost of formal methods growing "exponentially" with project size is clearly false.

by shasta 14y ago

deleted 14y ago
[deleted]
_delirium 14y ago
I wouldn't say "clearly" false, though it depends on what you mean by "cost". In a computational complexity sense, most methods are exponential, barring some special-case methods, though in practice you can scale up to pretty big problems anyway. For example, SMT solvers have complexity growing exponentially with the problem size, unless you greatly restrict the formalism, but can verify fairly large designs. The techniques I know of for verifying multithreaded programs have cost growing exponentially with the number of threads as well. He seems to be talking about proofs by hand, though, where you model a protocol mathematically and then write out a paper proving the protocol to be have desired properties. I have no idea if anyone's tried to quantify how that kind of complexity scales.
- shasta 14y ago
  I don't know how it scales either, but I'd guess that if your proofs grow even quadraticly with code size then you're doing something wrong. Exponential growth is just clearly wrong. Note that even for SMT solvers, there is not exponential growth with program size. Even with small programs, the model space can be infinite, and general automated theorem proving is undecidable, not NP. Do you have evidence that a million line program is inherently harder to check with an SMT solver than is a thousand line program? Both are probably jut checking approximations to the model. Similarly, with multi-threading, either the program works for a simple reason that it's author understands, or its correctness is not understood (and it probably doesn't work). People don't work through exponentially increasing number of cases in a growing project, and nor will formal proofs.
mynegation 14y ago
Do you have anything to substantiate your claim? I worked on formal methods and state explosion is a very real problem. The state of the program is essentially a subset of a Cartesian product of all variables. Even if all your 'n' variables are binary you still have a state space of potential size of 2^n.
- shasta 14y ago
  Right, and if your program uses a linked list, the state space is infinite! Correct programs written by humans are correct for reasons that don't require exhaustive case analysis.

The comment about the cost of formal methods growing "exponentially" with project size is clearly false.

by shasta 14y ago

The comment about the cost of formal methods growing "exponentially" with project size is clearly false.

deleted 14y ago

[deleted]

_delirium 14y ago

I wouldn't say "clearly" false, though it depends on what you mean by "cost". In a computational complexity sense, most methods are exponential, barring some special-case methods, though in practice you can scale up to pretty big problems anyway. For example, SMT solvers have complexity growing exponentially with the problem size, unless you greatly restrict the formalism, but can verify fairly large designs. The techniques I know of for verifying multithreaded programs have cost growing exponentially with the number of threads as well. He seems to be talking about proofs by hand, though, where you model a protocol mathematically and then write out a paper proving the protocol to be have desired properties. I have no idea if anyone's tried to quantify how that kind of complexity scales.

shasta 14y ago
I don't know how it scales either, but I'd guess that if your proofs grow even quadraticly with code size then you're doing something wrong. Exponential growth is just clearly wrong. Note that even for SMT solvers, there is not exponential growth with program size. Even with small programs, the model space can be infinite, and general automated theorem proving is undecidable, not NP. Do you have evidence that a million line program is inherently harder to check with an SMT solver than is a thousand line program? Both are probably jut checking approximations to the model. Similarly, with multi-threading, either the program works for a simple reason that it's author understands, or its correctness is not understood (and it probably doesn't work). People don't work through exponentially increasing number of cases in a growing project, and nor will formal proofs.

mynegation 14y ago

Do you have anything to substantiate your claim? I worked on formal methods and state explosion is a very real problem. The state of the program is essentially a subset of a Cartesian product of all variables. Even if all your 'n' variables are binary you still have a state space of potential size of 2^n.

shasta 14y ago
Right, and if your program uses a linked list, the state space is infinite! Correct programs written by humans are correct for reasons that don't require exhaustive case analysis.