Hacker News Reader

Comment by cryptica | Hacker News Reader

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.

View on HN

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.

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

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.

> 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?

While it's a good article, I didn't see it covering this aspect, particularly (c).

Would the code have been as clean and clear if you did not make the formal spec beforehand?

Yes

That's a problem with specs, the most concise and complete way to write them is by writing your program. If it wasn't, people would just compile the specs, and program using those.

Now, go tell this to people that want to offshore development based on a spec... But that's a digression.

You don't prove correctness of an entire program against the entire spec. That's only possible with toy problems, even entirely proved programs (like secL4) only prove some point of view, never the entire spec. Some times in a large program you discover a property that is very important (like how to assembly some event set into data, lack of deadlocks in a distributed system, or lack of buffers overflow), you then go and prove those properties.

> That's a problem with specs, the most concise and complete way to write them is by writing your program.

I've never dealt with formal specs/design, certainly nothing like those described here. Your comment (however in/accurate) strikes me as interesting and leads me to wonder...

What if we took the code and processed it to generate a "spec"? (I quote "spec" here b/c I wouldn't consider it a spec, but don't know what else to call it.) Basically, a document that explains verbosely what the written code does... hopefully in a way that is reasonably, humanly digestable.

Then we might get a doc that says, "Function add(...) accepts two integers/nulls and returns the sum." And Joe-coder looks and realizes it shouldn't accept nulls, goes back to the code, fixes the issue.

If there was a rule that functions could only return named variables (vs expressions that evaluate to a value that is returned) it would get closer to "this function accepts paramName1 and paramName2 and returns sumOfParams".

This is essentially what static code analysis attempts to do. Unfortunately, there are many ways of writing programs that today's static code analysis cannot understand.

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.

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.

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.

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

> 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.

False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.

It absolutely does. We studied SSADM in college.

> 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

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/ This is more "agile" than changing code between iterations.

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.

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

Reply on news.ycombinator.com