5 ms·

Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification

Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists.

Silhouette 8y ago
The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists. I think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations. There may be several levels of each, and the middle levels may overlap. For example, it may well be the case that the management on a project don't get heavily involved with the technical details and just specify "A needs to communicate with B" as part of the high level requirements. That doesn't mean the technical people responsible for implementing those requirement won't specify detailed protocols at a lower level and wouldn't benefit from formal methods to help ensure correct implementation.
- gaius 8y ago
  think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations Every government IT project that is years late and billions over budget is because of this
  - dragonwriter 8y ago
    > Every government IT project that is years late and billions over budget is because of this Well, that used to seem to be true before governments started experimenting with (methodologies which were notionally versions of) Agile, Lean, and related ideas. Then there were a whole new set of reasons for IT projects being years late and over budget.
  - aaaaaaaaaab 8y ago
    False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.
    - gaius 8y ago
      It absolutely does. We studied SSADM in college.
- kiriakasis 8y ago
  > it implies an often unrealistic separation between writing specs and writing implementations I think that part of the problem is that small modification in the spec can lead to enormous changes in the proofs
pytester 8y ago
I think it's worse than that. I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program. I wasn't really confident afterwards that the "proved" software actually did work. I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quickly the higher up the stack you go.
- mpweiher 8y ago
  I had exactly the same experience. We did specification in Z, but the code that was supposed to be "proved" correct was a clearer reflection of what we wanted to do than the "spec". So I actually had more confidence in the code than I did in the spec. And I think this answers the question of the OP: people don't use formal methods because (a) the vast majority of problems don't start out with a formal spec (b) the gap between informal and formal is vastly more relevant than the one between different formalisms (c) formal methods are significantly worse at bridging the formal/informal gap than most programming languages And yes, when you have a sub-problem that is mostly formal, then it can make sense, particularly if there's a lot riding on it.
  - brazzy 8y ago
    > And I think this answers the question of the OP Do you realize that the OP is actually linking to an article explaining this (and a bunch of other aspects) in great detail?
    - mpweiher 8y ago
      While it's a good article, I didn't see it covering this aspect, particularly (c).
- jononor 8y ago
  Would the code have been as clean and clear if you did not make the formal spec beforehand?
microcolonel 8y ago
I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before implementing it. I feel like there'd be more productivity in showing people what their code could do, and helping them narrow that down to what it should. It is, of course, hard to do this.
- kiriakasis 8y ago
  From this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more). Formal proof as in coq-proof are often not reasonable for many dynamic projects
walrus1066 8y ago
Indeed, I've never in my career (in high level businesses, I.e. Finance, advertising) seen such a thing as a proper 'specification'. It's more the business has a high level, rough idea of a change/feature to improve the business, and we figure out together the exact details, some of which surface during implementation, and then verify it gradually in the wild. We could have spent x10 time instead drawing up a formal spec up front, but it would have so many assumptions baked in, that it'd get invalidated in the wild anyway.
- craftinator 8y ago
  So the people designing the spec don't have enough information about the problem space. As the programmers begin working, they explore the problem space, extract the information they need to understand a solution, and then they can actually solve it. Bit of a Schrodinger's cat situation... The solution must remain undefined until observed.
pron 8y ago
But if you write some code, you must be writing it to do something. That something is your spec. This may or may not be what the customer wanted, but writing it down may make it easier to explain what it is that you've decided to implement, and understand whether or not it could be the right thing. Requirements do change constantly, which is all the more reason to write specs, so that you can understand the change and its implications (and present it to your customers) before writing the code. I am not saying this is always the best approach, but changing requirements in itself is not a reason not to use formal specification, but an additional motivation to use them. For example, this is a nice lightweight formal specification tool that allows to specify UI interactions quickly and play with them to see if they are satisfactory before implementing them: https://sketch.systems/ https://sketch.systems/ This is more "agile" than changing code between iterations.

Silhouette 8y ago

The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists. I think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations. There may be several levels of each, and the middle levels may overlap. For example, it may well be the case that the management on a project don't get heavily involved with the technical details and just specify "A needs to communicate with B" as part of the high level requirements. That doesn't mean the technical people responsible for implementing those requirement won't specify detailed protocols at a lower level and wouldn't benefit from formal methods to help ensure correct implementation.

gaius 8y ago
think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations Every government IT project that is years late and billions over budget is because of this
- dragonwriter 8y ago
  > Every government IT project that is years late and billions over budget is because of this Well, that used to seem to be true before governments started experimenting with (methodologies which were notionally versions of) Agile, Lean, and related ideas. Then there were a whole new set of reasons for IT projects being years late and over budget.
- aaaaaaaaaab 8y ago
  False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.
  - gaius 8y ago
    It absolutely does. We studied SSADM in college.
kiriakasis 8y ago
> it implies an often unrealistic separation between writing specs and writing implementations I think that part of the problem is that small modification in the spec can lead to enormous changes in the proofs

pytester 8y ago

I think it's worse than that. I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program. I wasn't really confident afterwards that the "proved" software actually did work. I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quickly the higher up the stack you go.

mpweiher 8y ago
I had exactly the same experience. We did specification in Z, but the code that was supposed to be "proved" correct was a clearer reflection of what we wanted to do than the "spec". So I actually had more confidence in the code than I did in the spec. And I think this answers the question of the OP: people don't use formal methods because (a) the vast majority of problems don't start out with a formal spec (b) the gap between informal and formal is vastly more relevant than the one between different formalisms (c) formal methods are significantly worse at bridging the formal/informal gap than most programming languages And yes, when you have a sub-problem that is mostly formal, then it can make sense, particularly if there's a lot riding on it.
- brazzy 8y ago
  > And I think this answers the question of the OP Do you realize that the OP is actually linking to an article explaining this (and a bunch of other aspects) in great detail?
  - mpweiher 8y ago
    While it's a good article, I didn't see it covering this aspect, particularly (c).
jononor 8y ago
Would the code have been as clean and clear if you did not make the formal spec beforehand?

microcolonel 8y ago

I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before implementing it. I feel like there'd be more productivity in showing people what their code could do, and helping them narrow that down to what it should. It is, of course, hard to do this.

kiriakasis 8y ago
From this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more). Formal proof as in coq-proof are often not reasonable for many dynamic projects

walrus1066 8y ago

Indeed, I've never in my career (in high level businesses, I.e. Finance, advertising) seen such a thing as a proper 'specification'. It's more the business has a high level, rough idea of a change/feature to improve the business, and we figure out together the exact details, some of which surface during implementation, and then verify it gradually in the wild. We could have spent x10 time instead drawing up a formal spec up front, but it would have so many assumptions baked in, that it'd get invalidated in the wild anyway.

craftinator 8y ago
So the people designing the spec don't have enough information about the problem space. As the programmers begin working, they explore the problem space, extract the information they need to understand a solution, and then they can actually solve it. Bit of a Schrodinger's cat situation... The solution must remain undefined until observed.

pron 8y ago

But if you write some code, you must be writing it to do something. That something is your spec. This may or may not be what the customer wanted, but writing it down may make it easier to explain what it is that you've decided to implement, and understand whether or not it could be the right thing. Requirements do change constantly, which is all the more reason to write specs, so that you can understand the change and its implications (and present it to your customers) before writing the code. I am not saying this is always the best approach, but changing requirements in itself is not a reason not to use formal specification, but an additional motivation to use them. For example, this is a nice lightweight formal specification tool that allows to specify UI interactions quickly and play with them to see if they are satisfactory before implementing them: https://sketch.systems/ https://sketch.systems/ This is more "agile" than changing code between iterations.