4 ms·

Formal methods don't make a lot of sense when the product changes from week to week, or month to month, or even year to year. It seems like the advocates of fo

Formal methods don't make a lot of sense when the product changes from week to week, or month to month, or even year to year. It seems like the advocates of formal methods assume a waterfall method of software development wherein you develop a spec, formalize it, prove that it works, and then deliver it. That's just not how software works in industry. A lot of it never had formal specs and never will, and whatever specs exist change frequently. By the time a spec is perfected it is out of date and we are already moving on to the next thing. Agile development killed waterfall development and formal methods have not adapted to the agile methodology.

Jtsummers 8y ago
Formal methods make sense when you focus them on the right part of your system. Even if it's changing week-to-week, there's an underlying structure or design that's staying consistent. You wouldn't use formal methods on, say, the GUI layout of your system. But you could use it to prove that you're accessing your database in a way that won't cause corrupted or incorrect data to appear. If you're working on anything with concurrency, this is actually crucial. Show, for instance, that your multi-user Google Docs clone won't end up with a corrupted document when two users try to edit the same sentence or word at the same time. That behavior won't change from week-to-week (both the multi-user nature and the desire for stability/reliability), though the nature of the interface or target platforms may change. Also, Waterfall only existed because some people at NASA/DOD were idiots and couldn't read past the intro to Royce's paper. It needs to die a terrible death. Formal methods can happily exist within an agile environment once you realize that you don't have to deliver code each week. You are able to deliver prototypes, mockups, and documents along the way. Formal models can exist in that group.
- adrianratnapala 8y ago
  > That behavior won't change from week-to-week Maybe "shouldn't" is a better world that "won't". It is sadly common for a sudden whim to cause a new feature to thread a change all the way from the GUI down to the database representation, with plumbing at multiple stages in the middle.
  - TeMPOraL 8y ago
    At GP's level of specification, things shouldn't change even then, unless you're doing an actual redefinition of what the software does and why. Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document".
    - logicchains 8y ago
      >Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document". What if you're building MongoDB a decade ago, and the new feature is "perform faster on benchmarks"?
      - AstralStorm 8y ago
        That is not a properly specified or useful requirement. 1) Your benchmarks have to be validated to correspond to real life usage. Especially problem sizes and specific structure. (Whether collisions are needed, what kind of queries etc.) 2) A proper performance specification is WCET or runtime histogram for given piece of code, which can be checked with a model checker. 3) It is a requirement to pass a given test "better". If that sounds good to your clients, well, you're selling a database to clueless people who somehow care about a specific benchmark... Competitors will pick a different benchmark to brag about. 4) Problematic parts of the code have to be identified, specified and fixed. And tested. If you do not match performance spec by then you have a different problem and need to redesign the software including algorithms used most likely. Very expensive.
  - craftinator 8y ago
    I think the use of formal methods on these key features would allow you to argue that they should not be changed. Giving more weight to resisting key feature change during initial development, as well as when the project matures and develops a user base, will help a lot with stabilization. That means less technical debt and fewer random breaking changes that tend to occur with Agile and other dynamic development practices.
- mshockwave 8y ago
  totally agree, formal specs usually used to describe the desired _goals_ of the project, so it's pretty high level and probably won't change pretty often
- nickpsecurity 8y ago
  "You wouldn't use formal methods on, say, the GUI layout of your system." That's actually a good use. Statecharts were one method used for formally specifying that. The research I saw would formally specify the individual components or modes, the transitions with their conditions, these would be checked formally, and then maybe some code is generated that's correct by construction. Example for prototyping: https://sketch.systems/ https://sketch.systems/
Tempacc78534 8y ago
Not True. Agile Dev (according to me) means you are trying to specify what the customer want as you develop your code and not specify it right in the beginning. You can make changes to the specs when you are figuring things out. Also, you do verification when you are somewhat confident in your code is doing what the customer wants, so verification should come towards the end of your development phase (or at least end of developing parts of your code base).
zzzcpan 8y ago
I don't think it's about agile, even with waterfall "you still don't know what you are actually making" as another comment put it. Making software is how you figure out what you are making. Formal methods are just philosophically incompatible with that. Software is how you learn the world and formal methods is how you create it, you can't have both and we don't really have much use for creating worlds.
pjmlp 8y ago
I wish it had killed waterfall, but the large majority of enterprise customers I have dealt with, see it differently.
rtpg 8y ago
Some things change, others stay the same. You change the system, and now some part of the application works differently. The way for you to determine if it's expected or not is through the spec of the system. Either it's a bug to have changed it or it wasn't. In theory, you can use stuff like formal methods while changing a system when you come across things that you think _shouldn't_ change. It's the same concept as tests, really. In practice I have not found any good tooling for this in production systems. The best alternatives are using types to enforce some rules, and to make APIs that make expressing invalid state impossible. But this is only a small subset of the kind of guarantees you want to have.
gaius 8y ago
That's just not how software works in industry. If by industry you mean “webdev” but fortunately “full stack engineers” don’t work on avionics or indeed anything important.
ummonk 8y ago
I'm not sure that is necessarily true. I think of the modern typechecker (especially with generics, algebraic data types, and other advanced features, including sometimes dependent tpes) as basically formal-verification-lite, and it tends to work really well with changing specs. You can aggressively refactor and change code and just let the compiler catch errors as you go. A practical formal verification language would function much the same way.
- alexisread 8y ago
  This! I'd also argue that your formal verification language and your coding language are one and the same. This leads to the case where if you can specify your language, it is written. Obviously there are scenarios where it's not practical to prove a part of the program, but you can simply use an unsafe dialect as per Rust or Maude (system modules). This works well with agile development in that you can spec out the underlying communications protocols, parallel operations etc. and layer unsafe stuff on top. While we're here then, being able to publish these proven modules for other people should lead to a situation where we can build incrementally on code proofs. Lastly, you can consider this system to be the equivalent of unit tests, but better in that there are guaranteed to be no edge cases you haven't tested (subject to coverage, but again publishing modules should help bullet-proof them). For integration testing, you can use behavioural proofs - see Maude or BOBJ.
pron 8y ago
Do unit tests or type systems make sense when the product changes from week to week? Unit tests and type systems are a formal method (technically; usually they usually do not fall under the academic discipline of formal methods). Formal methods cover a very wide range of tools, that drastically differ in cost and effort. Also, if you have code, then you have a spec, because the code is itself a formal specification. It's just not a very convenient one because it is a very low-level spec.

Jtsummers 8y ago

Formal methods make sense when you focus them on the right part of your system. Even if it's changing week-to-week, there's an underlying structure or design that's staying consistent. You wouldn't use formal methods on, say, the GUI layout of your system. But you could use it to prove that you're accessing your database in a way that won't cause corrupted or incorrect data to appear. If you're working on anything with concurrency, this is actually crucial. Show, for instance, that your multi-user Google Docs clone won't end up with a corrupted document when two users try to edit the same sentence or word at the same time. That behavior won't change from week-to-week (both the multi-user nature and the desire for stability/reliability), though the nature of the interface or target platforms may change. Also, Waterfall only existed because some people at NASA/DOD were idiots and couldn't read past the intro to Royce's paper. It needs to die a terrible death. Formal methods can happily exist within an agile environment once you realize that you don't have to deliver code each week. You are able to deliver prototypes, mockups, and documents along the way. Formal models can exist in that group.

adrianratnapala 8y ago
> That behavior won't change from week-to-week Maybe "shouldn't" is a better world that "won't". It is sadly common for a sudden whim to cause a new feature to thread a change all the way from the GUI down to the database representation, with plumbing at multiple stages in the middle.
- TeMPOraL 8y ago
  At GP's level of specification, things shouldn't change even then, unless you're doing an actual redefinition of what the software does and why. Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document".
  - logicchains 8y ago
    >Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document". What if you're building MongoDB a decade ago, and the new feature is "perform faster on benchmarks"?
    - AstralStorm 8y ago
      That is not a properly specified or useful requirement. 1) Your benchmarks have to be validated to correspond to real life usage. Especially problem sizes and specific structure. (Whether collisions are needed, what kind of queries etc.) 2) A proper performance specification is WCET or runtime histogram for given piece of code, which can be checked with a model checker. 3) It is a requirement to pass a given test "better". If that sounds good to your clients, well, you're selling a database to clueless people who somehow care about a specific benchmark... Competitors will pick a different benchmark to brag about. 4) Problematic parts of the code have to be identified, specified and fixed. And tested. If you do not match performance spec by then you have a different problem and need to redesign the software including algorithms used most likely. Very expensive.
- craftinator 8y ago
  I think the use of formal methods on these key features would allow you to argue that they should not be changed. Giving more weight to resisting key feature change during initial development, as well as when the project matures and develops a user base, will help a lot with stabilization. That means less technical debt and fewer random breaking changes that tend to occur with Agile and other dynamic development practices.
mshockwave 8y ago
totally agree, formal specs usually used to describe the desired _goals_ of the project, so it's pretty high level and probably won't change pretty often
nickpsecurity 8y ago
"You wouldn't use formal methods on, say, the GUI layout of your system." That's actually a good use. Statecharts were one method used for formally specifying that. The research I saw would formally specify the individual components or modes, the transitions with their conditions, these would be checked formally, and then maybe some code is generated that's correct by construction. Example for prototyping: https://sketch.systems/ https://sketch.systems/

Tempacc78534 8y ago

Not True. Agile Dev (according to me) means you are trying to specify what the customer want as you develop your code and not specify it right in the beginning. You can make changes to the specs when you are figuring things out. Also, you do verification when you are somewhat confident in your code is doing what the customer wants, so verification should come towards the end of your development phase (or at least end of developing parts of your code base).

zzzcpan 8y ago

I don't think it's about agile, even with waterfall "you still don't know what you are actually making" as another comment put it. Making software is how you figure out what you are making. Formal methods are just philosophically incompatible with that. Software is how you learn the world and formal methods is how you create it, you can't have both and we don't really have much use for creating worlds.

pjmlp 8y ago

I wish it had killed waterfall, but the large majority of enterprise customers I have dealt with, see it differently.

rtpg 8y ago

Some things change, others stay the same. You change the system, and now some part of the application works differently. The way for you to determine if it's expected or not is through the spec of the system. Either it's a bug to have changed it or it wasn't. In theory, you can use stuff like formal methods while changing a system when you come across things that you think _shouldn't_ change. It's the same concept as tests, really. In practice I have not found any good tooling for this in production systems. The best alternatives are using types to enforce some rules, and to make APIs that make expressing invalid state impossible. But this is only a small subset of the kind of guarantees you want to have.

gaius 8y ago

That's just not how software works in industry. If by industry you mean “webdev” but fortunately “full stack engineers” don’t work on avionics or indeed anything important.

ummonk 8y ago

I'm not sure that is necessarily true. I think of the modern typechecker (especially with generics, algebraic data types, and other advanced features, including sometimes dependent tpes) as basically formal-verification-lite, and it tends to work really well with changing specs. You can aggressively refactor and change code and just let the compiler catch errors as you go. A practical formal verification language would function much the same way.

alexisread 8y ago
This! I'd also argue that your formal verification language and your coding language are one and the same. This leads to the case where if you can specify your language, it is written. Obviously there are scenarios where it's not practical to prove a part of the program, but you can simply use an unsafe dialect as per Rust or Maude (system modules). This works well with agile development in that you can spec out the underlying communications protocols, parallel operations etc. and layer unsafe stuff on top. While we're here then, being able to publish these proven modules for other people should lead to a situation where we can build incrementally on code proofs. Lastly, you can consider this system to be the equivalent of unit tests, but better in that there are guaranteed to be no edge cases you haven't tested (subject to coverage, but again publishing modules should help bullet-proof them). For integration testing, you can use behavioural proofs - see Maude or BOBJ.

pron 8y ago

Do unit tests or type systems make sense when the product changes from week to week? Unit tests and type systems are a formal method (technically; usually they usually do not fall under the academic discipline of formal methods). Formal methods cover a very wide range of tools, that drastically differ in cost and effort. Also, if you have code, then you have a spec, because the code is itself a formal specification. It's just not a very convenient one because it is a very low-level spec.