4 ms·

Exactly. Even assuming (3) is true you've just pushed the problem down to your spec.

by JackFr 10y ago

zzzcpan 10y ago
Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.
- philipkglass 10y ago
  Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.
  - nickpsecurity 10y ago
    I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf
nickpsecurity 10y ago
Which is great given they're precise statements about what you want to do that are easier for humans and computers to analyze. They don't have the language-level problems either. Tools can then turn those into code or do much of the work from there.
jfoutz 10y ago
If your spec is wrong, your code will be wrong anyway. More often, people use the code as the spec which is IMHO (for this kind of programing) really bad.

Exactly. Even assuming (3) is true you've just pushed the problem down to your spec.

by JackFr 10y ago

Exactly. Even assuming (3) is true you've just pushed the problem down to your spec.

Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.

philipkglass 10y ago
Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.
- nickpsecurity 10y ago
  I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf

nickpsecurity 10y ago

Which is great given they're precise statements about what you want to do that are easier for humans and computers to analyze. They don't have the language-level problems either. Tools can then turn those into code or do much of the work from there.

jfoutz 10y ago

If your spec is wrong, your code will be wrong anyway. More often, people use the code as the spec which is IMHO (for this kind of programing) really bad.