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

171–180 of 232 posts

Re: Why Don't People Use Formal Methods?

#171

Post by blattimwind »

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…

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

This was historically and still is largely false. A mathematical proof is a written argument and most proofs are too complex to be "obviously correct", therefore mathematical proofs are usually more like your latter case: It is an argument that convinces people. Mathematics has a long history of doing things "that sound right but haven't been proven yet but it seems to work out ok", e.g. this was done all the time in the earlier days of analysis.

Re: Why Don't People Use Formal Methods?

#172

Post by mpweiher »

brazzy wrote: post #153
mpweiher wrote: post #136

Earlier quoted context omitted.

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

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

Re: Why Don't People Use Formal Methods?

#173

Post by kiriakasis »

UncleMeat wrote: post #30
zozbot123 wrote: post #13

> Why Don't People Use Formal Methods? Because they're an emerging and unproven technology? Why don't people rewrite everything in Rust? That would surely be a lot more straightforward than adopting the sorts of "formal methods" where you only write a handful of (C-language equivalent) LOC per day, across the software industry! So why doesn't it happen? There's your answer.

Static type checking is abstract interpretation. If you program in Java you are using formal methods.

The proofs you produce are probably weaker than those the author wants

Re: Why Don't People Use Formal Methods?

#174

Post by pytester »

jononor wrote: post #165
pytester wrote: post #123

Earlier quoted context omitted.

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

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

Yes

Re: Why Don't People Use Formal Methods?

#175

Post by Uberphallus »

patates wrote: post #147
pasta wrote: post #138

Earlier quoted context omitted.

I sometimes feel this also a language or tool problem. For example an integer. In most languages and tools this is a primitive. But most of the time we need a specific type of integer, for example a positive natural number. You can use a unsigned integer for this but that will include a zero wich we don't want. So maybe you can use a type/domain object for this in your code, but what about the database field or commu…

Ada has subtypes for such cases: https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Co...

And checks on compile time are quite insightful, Ada tends to know beforehand if you're gonna run out of bounds.

Re: Why Don't People Use Formal Methods?

#176

Post by dranov »

iso-8859-1 wrote: post #163
dranov wrote: post #135

Earlier quoted context omitted.

I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently extending that work for my Master's thesis. Others are also building on top of that work [3]. We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation),…

First you mention Nakamoto consensus, then you mention "existing consensus code". Are you including Bitcoin script when you say consensus? It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. How would you replicate something like the BIP-0050 problem? https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...

> Are you including Bitcoin script when you say consensus?

Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions.

However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state.

The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however.

> It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR.

It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.)

I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.

Re: Why Don't People Use Formal Methods?

#177

Post by brohee »

blub wrote: post #116
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…

A good ligature font solves those...

Re: Why Don't People Use Formal Methods?

#178

Post by Jtsummers »

verinus wrote: post #155
Jtsummers wrote: post #59

Earlier quoted context omitted.

I'll disagree, I don't think they're making a good point. GP implies that formal methods always add time to projects, which is going to be true for: 1) Projects that are building the wrong thing and spend time verifying the wrong thing (failed validation) 2) Projects with people inexperienced in formal methods (most projects today) The latter is just a matter of experience. Once people get used to thinking about thin…

well if I read you correctly he IS making a good point: > 2) Projects with people inexperienced in formal methods (most projects today) which is exactly what matters and what adds a lot of time to dev. 1) cannot be addressed by formal method and is one of the most important things when building software.

It’s a temporary problem, not a permanent problem. People need training and practice. I’d expect most people were slower when first using unit tests or TDD than they are today. It takes time to build that experience into the industry but it’s hardly an impossible problem. Especially as the tooling (PlusCal, Alloy) for lighter weight formal methods gets better and more accessible.

Re: Why Don't People Use Formal Methods?

#179

Post by chii »

pasta wrote: post #138
tanilama wrote: post #129

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

I sometimes feel this also a language or tool problem. For example an integer. In most languages and tools this is a primitive. But most of the time we need a specific type of integer, for example a positive natural number. You can use a unsigned integer for this but that will include a zero wich we don't want. So maybe you can use a type/domain object for this in your code, but what about the database field or commu…

Or, don't split between primitives vs objects.

I think it's a mistake to make thet distinction in many language's design.

Post reply on HN