Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why Don't People Use Formal Methods?

hillelwayne.com

Post reply on HN
Print view View original

111–120 of 232 posts

Re: Why Don't People Use Formal Methods?

#111

Post by Symbiote »

roenxi wrote: post #107
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…

There is a substantial language barrier; articles like this keep using the word 'proof', and I can't figure out what they mean. Each discipline has it's own standards of proof. In mathematics, the word means that a statement transcends the laws of time and space. In law, it means a group of 'reasonable people' can be convinced. In science it means that there is a theory with supporting data that has not been falsifie…

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.

Re: Why Don't People Use Formal Methods?

#112

Post by dragonwriter »

gaius wrote: post #106
Silhouette wrote: post #97

Earlier quoted context omitted.

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…

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.

Re: Why Don't People Use Formal Methods?

#113

Post by baybal2 »

I think all formal verification methods are built from bottom up, and verification begins at standard C library. The bigger you program gets, the more dependencies you have to verify.

If your tech platform does not have a long history of formal methods, you will have hard time building the verification chain on your own.

In Javascript, for example, you will have to formally verify the whole browser, and all its dependencies, before you can meaningfully verify the code running inside it. That's very hard

Re: Why Don't People Use Formal Methods?

#114

Post by [deleted] »

statguy wrote: post #103

Surprised that no one has mentioned this yet https://www.joelonsoftware.com/2005/01/02/advice-for-compute... > After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, th…

[deleted]

Re: Why Don't People Use Formal Methods?

#115

Post by roenxi »

Symbiote wrote: post #111
roenxi wrote: post #107

Earlier quoted context omitted.

There is a substantial language barrier; articles like this keep using the word 'proof', and I can't figure out what they mean. Each discipline has it's own standards of proof. In mathematics, the word means that a statement transcends the laws of time and space. In law, it means a group of 'reasonable people' can be convinced. In science it means that there is a theory with supporting data that has not been falsifie…

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 fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway. So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing? That is a debatable point, and the economics suggests no.

Since formal methods are clearly targeted at programming, what is this link to software? We can prove trivial things like 1+1=2 but that still doesn't necessarily connect to anything that gets implemented.

Any program is a trivial proof of itself; so why are we interested in these specific proofs? Saying that they have a proof doesn't seem meaningful and is a language barrier to whatever they actually mean - which having had a good long think, is probably 'programmatic scoping', which describes what they actually seem to be doing.

Re: Why Don't People Use Formal Methods?

#116

Post by blub »

xvilka wrote: post #45

Part of the problem is that TLA+ syntax and tooling is horrendous. Creating something more modern and widely adoptable is a key for Mass scale applications.

TLA+ is an ugly language, just like PlusCal. I'll never understand how people can come to the conclusion that it's fine to have syntax like:

* \A p \in people

* acc = [p \in people |-> 5]

* (-- ;) for wrapping PlusCal

* /= for inequality

* /\ for and

* seq1 \o seq2 for append

* and so on

All of these are from the Practical TLA+ book.

Honestly, TLA+ (or PlusCal) looks very impractical. If I want to use mathematical notation I'll do on paper, not write some frankenstein version of it in Eclipse.

At this point the whole syntax should be written off as a failed experiment and they should kindly ask Anders Hejlsberg or Guido van Rossum for help.

Re: Why Don't People Use Formal Methods?

#117

Post by dmitriid »

agumonkey wrote: post #86
kod wrote: post #79

Earlier quoted context omitted.

Standard ML has existed for 35 years. Even if you started programming with Fortran, it's been around longer than half of your career.

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"

Re: Why Don't People Use Formal Methods?

#118

Post by ummonk »

Most software complexity is in interactions between systems. Container frameworks, operating system, hardware drivers, random libraries, 3rd party APIs, cloud provider APIs, client browser, etc.

Unless all of these are specified in a single language / framework, you can't really apply formal methods to the system. Instead you'll only be applying formal methods to individual library functions / features. At least for code that isn't security-critical, these are already quite robust thanks to the use of strong typing (especially with powerful typecheckers for algebraic data types) and unit testing. Formal methods are merely an improvement on advanced typecheckers and unit testing frameworks.

The real difficulty is in verifying complex interacting systems - the kind of thing for which you have integration tests, which are quite difficult to write in an exhaustive way and catch edge conditions.

Note also that even for security-critical code, formal methods don't really guarantee safety either, since many classes of attacks are based on timing attacks, especially cache-based timing attacks.

Re: Why Don't People Use Formal Methods?

#119

Post by aaaaaaaaaab »

gaius wrote: post #106
Silhouette wrote: post #97

Earlier quoted context omitted.

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…

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

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

Re: Why Don't People Use Formal Methods?

#120

Post by jonathanstrange »

Most of the answers already given are good, but there is a simpler one: It's too expensive.

It's so expensive that even the highly regulated and safety aware aerospace industry avoids formal verification for non-essential systems when they are allowed to.

Moreover, formal verification only makes sense in combination with certifying the software on some specific hardware, because it would be a pointless waste of time to run software that is guaranteed to behave well on hardware that makes no guarantees that it will execute the software correctly. Consequently, even small changes in hardware may force you to re-evaluate the whole system. So the maintenance costs of high integrity systems are also very high.

Post reply on HN