3 ms·

This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to re

by nmrm2 11y ago

This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.

pron 11y ago
> The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
- nmrm2 11y ago
  My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
jessaustin 11y ago
...disingenious. English usage note: if the word you meant to use was "disingenuous", I would suggest "spurious" instead, as it expresses similar feelings about "this distinction", without also attributing unsavory motives to 'pron.
- ScottBurson 11y ago
  Hey, I like this word "disingenious". I think it could mean "a bad idea being promulgated to displace (what the speaker considers) a much better idea". We need a word for that :-)
eli_gottlieb 11y ago
>The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. How many zero-day security flaws have to occur in core infrastructure like, for instance, OpenSSH before the laziness of engineers about learning "academic" tools stops being a cost-effective excuse not to use formal methods?

by nmrm2 11y ago

pron 11y ago

> The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.

nmrm2 11y ago
My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.

jessaustin 11y ago

...disingenious. English usage note: if the word you meant to use was "disingenuous", I would suggest "spurious" instead, as it expresses similar feelings about "this distinction", without also attributing unsavory motives to 'pron.

ScottBurson 11y ago
Hey, I like this word "disingenious". I think it could mean "a bad idea being promulgated to displace (what the speaker considers) a much better idea". We need a word for that :-)

eli_gottlieb 11y ago

>The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. How many zero-day security flaws have to occur in core infrastructure like, for instance, OpenSSH before the laziness of engineers about learning "academic" tools stops being a cost-effective excuse not to use formal methods?