Why Don't People Use Formal Methods? • Hacker News Board

Re: Why Don't People Use Formal Methods?

#121

Post by phtrivier » Tue, Jan 22, 2019, 9:02 AM UTC

I might be missing something obvious, but from my (small) reading about TLA+ (and the lamport video course), my biggest concerns were:

A: even if you understand the spec you want to write, it's possible to get the implementation of the spec in the spec language wrong (see the Die Hard exercise in the course) ; isn't there some kind of recursive catch-22 there ?

B: even if you understand the spec you want to write, and manage to write the spec you want to write, and get its model checked, etc... Than you still have 0 lines of working code, and (unless I'm mistaken) you're going to have plenty of occasions to not implement the spec properly, and still get all the bugs that you proved would not happen if you had written the code right (you dummy.)

So it seems like the interesting part is the "game of thinking harder about what you want to do", and it is (arguably) done (at least in part) by writing automated tests beforehand, and the tests also have value after you've written the production code.

That at least could explain why the jump to formal method is not natural.

Looking forward to being wrong, though.

Re: Why Don't People Use Formal Methods?

#122

Post by ummonk » Tue, Jan 22, 2019, 9:03 AM UTC

twblalock wrote: post #26

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 sp…

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.

Re: Why Don't People Use Formal Methods?

#123

Post by pytester » Tue, Jan 22, 2019, 9:10 AM UTC

cryptica wrote: post #93

mikekchar wrote: post #53

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…

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 ex…

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.

Re: Why Don't People Use Formal Methods?

#124

Post by microcolonel » Tue, Jan 22, 2019, 9:10 AM UTC

cryptica wrote: post #93

mikekchar wrote: post #53

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…

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 ex…

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.

Re: Why Don't People Use Formal Methods?

#125

Post by orbifold » Tue, Jan 22, 2019, 9:12 AM UTC

roenxi wrote: post #115

Symbiote wrote: post #111

Earlier quoted context omitted.

Proof in formal methods means the mathematical kind: with certainty the program / function implements the specification. Mathematicians can also prove something irrelevant or useless, or something fundamental like 1+1=2.

Well, yes, but if mathematicians prove something then we know it is true. And if they can't prove the trivialities, that would be a crisis for the entire discipline, because 1+1=2 relates to everything they do. If software people prove something we also know it is true, but not that it usefully relates to the software. In fact, 0.1+0.2 is likely != 0.3 for most software. You can prove you have integer types or fracti…

Although it is not self evident from looking at most modern software, prgogramming and proofs are (in some instances) direclty related by the Curry-Howard correspondence. Apart from such instances one can also try to assert temporal relationships between variables in a program that have to hold under all inputs (one example would be “valid until ready”, which is a typical requirement one would have for a queue interface: the producer can not revoke the claim that the data is valid until the consumer has accepted it). Such assertions can be verified with TLA+ or in System Verilog with tools such as Formality.

Re: Why Don't People Use Formal Methods?

#126

Post by logicchains » Tue, Jan 22, 2019, 9:17 AM UTC

twic wrote: post #80

throwawayjava wrote: post #64

Earlier quoted context omitted.

> The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. The world is changing. In high-growth-potential areas, I think we're starting to see a shift away from the style of software where "what to build is hard but how to build is easier" and toward a…

> automated trading > It's really obvious what we want the system to do Nope.

Buy low, sell high!

Re: Why Don't People Use Formal Methods?

#127

Post by logicchains » Tue, Jan 22, 2019, 9:20 AM UTC

TeMPOraL wrote: post #77

adrianratnapala wrote: post #51

Earlier quoted context omitted.

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

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

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

Re: Why Don't People Use Formal Methods?

#128

Post by walrus1066 » Tue, Jan 22, 2019, 9:20 AM UTC

cryptica wrote: post #93

mikekchar wrote: post #53

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…

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 ex…

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.

Re: Why Don't People Use Formal Methods?

#129

Post by tanilama » Tue, Jan 22, 2019, 9:20 AM UTC

If you want certain technology to be commercially successful, it needs to provide value.

For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests.

However, in different scenarios, like financial trading or consistency protocol building, where a single mistake will either cause you millions or resulting in nonrecoverable data loss that make customers lose confidence in your product, formal methods ARE indeed being used.

So it is simply a cost efficiency problem. For most disposable application project, it is not worth it, so they don't invest. If the code of interests is critical, and deserve every effort to get it right, then formal methods will be favored.

Re: Why Don't People Use Formal Methods?

#130

Post by agumonkey » Tue, Jan 22, 2019, 9:21 AM UTC

dmitriid wrote: post #117

agumonkey wrote: post #86

Earlier quoted context omitted.

Be honest, until 10y ago, ml type inference was invisible to 90% of the coders. Probably rejected willingly even ('where are my objects?')

> Probably rejected willingly even ('where are my objects?') Local type inference was rejected in Java in 2001 because "you need to spec your types precisely"

is it published online ?