3 ms·

Whether or not formal methods can be applied is almost entirely an economic decision since that kind of rigor drives up cost. Makes sense in certain high value

Whether or not formal methods can be applied is almost entirely an economic decision since that kind of rigor drives up cost. Makes sense in certain high value systems when the organization wrapped around them has the resources or the level of risk associated with a less rigorous approach is too high (e.g. at NASA). What the author seems to miss completely is that there are many systems developed using typical methodologies that generate billions in revenue. What this tells you is that ideas like TLA+ are effectively superfluous in a wide variety of software contexts.

bhaak 5y ago
It's not easy to quantify but you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate. How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP.
- bobthechef 5y ago
  I don't think the OP dismisses formal methods, only the idea that they have pervasive utility that outweighs costs in most scenarios, at least for certain kinds of formal methods. But we can't forget the range of formal methods either. Type systems technically qualify, as the article notes, even if they are lightweight, and they're not new. Given the pervasiveness of Java, we're already making widespread use of at least that formal method and have been for a long time. > How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP. The OP wasn't arguing that revenue is driving or should drive language selection, only that the revenue shows that the lack of formal methods does not seems to prevent companies from making enormous sums of money. > you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate. That by itself is not much of a positive argument for their use. And do you know how much maintenance overhead they would introduce? In either case, it might be useful to compare how a switch between similar languages (e.g. JS and Typescript) affected code quality (in terms of the number of bug reports filed, for example) and feature delivery time. Maybe there's a point where the trade off makes sense. In which case, languages that support a gradual adoption of formal methods might begin to look attractive.
- oneplane 5y ago
  The programming language itself has very little to do with the revenue something generates. Revenue isn't generated by technical details, those are just the implementation of a product that itself is just an implementation of the goals of the business. The reason people are and aren't programming in PHP is just plain and simple: taste. Maybe ff 10 developers in a team want to use PHP they can just do that, as long as at the end of the line the product delivers. If 3/10 want to use PHP, and 7/10 want to use C# then no, it will not likely run on PHP. And if as a developer you prefer certain features or tools over others, you are likely to select the technologies that suit that. None of the technical details had anything to do with the value that was created. If your requirements say that 100 people per minute need to be able to find, basket and purchase product on a website, and those requirements are met, does it really matter if the codebase is a combination of AppleScript and an ActiveX control? (I know, that technically doesn't exist, not the point) Now, if those requirements also include scaling needs, long-term support needs, knowledge sharing, consultancy options, then you might not select those technologies.
ntietz 5y ago
I mean, it depends on criticality. If something is critical, pushing further along the formal methods spectrum makes sense (see also: why AWS has done a lot with TLA+). Sure, we probably won’t verify all of Instagram, but super critical portions of the platform underlying it are likely worth it and would save money in the long run by reducing outages, bugs, etc.
- MaxBarraclough 5y ago
  I'm fond of formal methods, but I'll offer the usual counter-example: Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply). As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.
  - TheOtherHobbes 5y ago
    It's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements. A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.
andrekandre 5y ago
also, they dont mean bunk if business side of the equation isnt behind them... following formal methods means that business also follows formal business methods (which would reduce sudden changes and mistaken product designs etc). too many times "dev" is treated like a roving circus that can just change their routine on a dime with little consequences...

bhaak 5y ago

It's not easy to quantify but you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate. How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP.

bobthechef 5y ago
I don't think the OP dismisses formal methods, only the idea that they have pervasive utility that outweighs costs in most scenarios, at least for certain kinds of formal methods. But we can't forget the range of formal methods either. Type systems technically qualify, as the article notes, even if they are lightweight, and they're not new. Given the pervasiveness of Java, we're already making widespread use of at least that formal method and have been for a long time. > How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP. The OP wasn't arguing that revenue is driving or should drive language selection, only that the revenue shows that the lack of formal methods does not seems to prevent companies from making enormous sums of money. > you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate. That by itself is not much of a positive argument for their use. And do you know how much maintenance overhead they would introduce? In either case, it might be useful to compare how a switch between similar languages (e.g. JS and Typescript) affected code quality (in terms of the number of bug reports filed, for example) and feature delivery time. Maybe there's a point where the trade off makes sense. In which case, languages that support a gradual adoption of formal methods might begin to look attractive.
oneplane 5y ago
The programming language itself has very little to do with the revenue something generates. Revenue isn't generated by technical details, those are just the implementation of a product that itself is just an implementation of the goals of the business. The reason people are and aren't programming in PHP is just plain and simple: taste. Maybe ff 10 developers in a team want to use PHP they can just do that, as long as at the end of the line the product delivers. If 3/10 want to use PHP, and 7/10 want to use C# then no, it will not likely run on PHP. And if as a developer you prefer certain features or tools over others, you are likely to select the technologies that suit that. None of the technical details had anything to do with the value that was created. If your requirements say that 100 people per minute need to be able to find, basket and purchase product on a website, and those requirements are met, does it really matter if the codebase is a combination of AppleScript and an ActiveX control? (I know, that technically doesn't exist, not the point) Now, if those requirements also include scaling needs, long-term support needs, knowledge sharing, consultancy options, then you might not select those technologies.

ntietz 5y ago

I mean, it depends on criticality. If something is critical, pushing further along the formal methods spectrum makes sense (see also: why AWS has done a lot with TLA+). Sure, we probably won’t verify all of Instagram, but super critical portions of the platform underlying it are likely worth it and would save money in the long run by reducing outages, bugs, etc.

MaxBarraclough 5y ago
I'm fond of formal methods, but I'll offer the usual counter-example: Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply). As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.
- TheOtherHobbes 5y ago
  It's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements. A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.

andrekandre 5y ago

also, they dont mean bunk if business side of the equation isnt behind them... following formal methods means that business also follows formal business methods (which would reduce sudden changes and mistaken product designs etc). too many times "dev" is treated like a roving circus that can just change their routine on a dime with little consequences...