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

Re: Why Don't People Use Formal Methods?

#181

Post by [deleted] » Tue, Jan 22, 2019, 12:51 PM UTC

pytester wrote: post #123

cryptica wrote: post #93

Earlier quoted context omitted.

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

[deleted]

Re: Why Don't People Use Formal Methods?

#182

Post by xiphias2 » Tue, Jan 22, 2019, 1:20 PM UTC

dranov wrote: post #135

xiphias2 wrote: post #41

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well:…

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),…

It looks interesting, but I believe even verifying 100-200 lines in the real Bitcoin consensus code is more useful. All the Bitcoin Core developers know that the Bitcoin implementation is a mess, but they understood that it's just not going away. As for Bitcoin script, there's a plan to upgrade it to Simplicity (https://blockstream.com/simplicity.pdf), but even then, the old code will stay (there's a concensus that there won't be any hard forks for a long time unless it's really needed).

The last bug was in the caching code (a transaction could slip twice in a block which could lead to inflation), and it was something that only formal verification of inflation in the current code would catch.

My biggest worry is with digital signatures in the Bitcoin blockchain: if there's a bug in it, it's over, building trust again is extremely hard.

Re: Why Don't People Use Formal Methods?

#183

Post by Graham24 » Tue, Jan 22, 2019, 1:22 PM UTC

when I was at university we did a module on Formal Methods including writing Z Schemas. Out of a class of 30 only two people really understood them.

That's why they are not generally used, no one (or at least not enough) has a clue how to create them.

I doubt they are taught on general Computer Science degrees anymore.

Re: Why Don't People Use Formal Methods?

#184

Post by xiphias2 » Tue, Jan 22, 2019, 1:23 PM UTC

DoctorOetker wrote: post #84

xiphias2 wrote: post #41

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well:…

Almost 10 years ago on bitcoin dev IRC channel I was asking the devs to consider having the reference specification to be formally specified, so that all clients, are at least supposed / expected to comply with it. They were not interested...

The problem is that there's no such thing as a formal specification when running C++ code, and I believe Coq runs too slow to be practical. We have Rust now as an alternative language, but it's too late to rewrite the consensus code, so we have to work with legacy code.

Re: Why Don't People Use Formal Methods?

#185

Post by LeeJMiller » Tue, Jan 22, 2019, 1:42 PM UTC

my buddy's friend makes $96 hourly on the internet. She has been with out artwork for five months however final month her charge emerge as $12747 really on foot on the internet for some hours. study greater on this net internet site... HERE.......www.moneytechs.com

Re: Why Don't People Use Formal Methods?

#186

Post by chriswarbo » Tue, Jan 22, 2019, 1:50 PM 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…

> In fact, 0.1+0.2 is likely != 0.3 for most software.

This seems like a rather silly example: you're presumably talking about floating point numbers, but we have a spec for floating point, it's IEEE 754. This spec has been formalised in many proof systems, e.g. (top Google hits for various systems I know):

  https://github.com/coq-contribs/ieee754

  https://agda.readthedocs.io/en/v2.5.4/language/built-ins.html#floats

  https://www.isa-afp.org/entries/IEEE_Floating_Point.html

I'm tempted to say that using integers/rationals/reals in a proof, when the software uses 64bit words and floats, is a rookie mistake; yet I've never even seen rookies make that mistake. Maybe that's a problem for approaches which keep programs and proofs separate, but in systems based on type-checking (e.g. Agda and Coq) it wouldn't even be possible to make such a mistake (there's no way to use different types in the program and the proof, since the program is the proof).

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

I'd be very happy if hardware bugs were the main cause of my software's problems ;) More seriously, this seems like moving the goalposts from "is it useful?" to "is it perfect?".

Re: Why Don't People Use Formal Methods?

#187

Post by School-Cotton » Tue, Jan 22, 2019, 2:13 PM UTC

jacques_chester wrote: post #6

The trite answer is: because it's hard. (An entire section in the article is devoted to this point.) Programming languages and tooling have attracted phenomenal amounts of attention and iteration in just a few decades. Folks hereabouts just about go to the damn mats over the smallest syntactic quibbles. Meanwhile, over in mathematician land, they're limping along with a write-optimised mishmash of "the first thing th…

I think this is an exaggeration/strawman. Can you give an example of a mainstream introductory math book that defines some esoteric notation like "Q(x)" and then continues using it hundreds of pages later? Note that I don't mean defining it locally within the context of one proof -- that's something different.

The closest thing I can think of is notations like U(f, P) and L(f, P) for the upper and lower Riemann sums of a function f with respect to a partition P. These do show up in introductory real analysis textbooks, but they're pretty basic/fundamental notions.

By the way, as far as I know, ∂ in introductory textbooks can only mean either "partial derivative" or "boundary". Do you have examples of it meaning other things?

Re: Why Don't People Use Formal Methods?

#188

Post by your-nanny » Tue, Jan 22, 2019, 2:15 PM UTC

jacques_chester wrote: post #6

The trite answer is: because it's hard. (An entire section in the article is devoted to this point.) Programming languages and tooling have attracted phenomenal amounts of attention and iteration in just a few decades. Folks hereabouts just about go to the damn mats over the smallest syntactic quibbles. Meanwhile, over in mathematician land, they're limping along with a write-optimised mishmash of "the first thing th…

Math is hard, and reading it is slow for even ggood mathmeticians. However, it does get easier with practice, as one learns the conventions and norms. It is not self explanatory; aliens would not glance at a notebook and immediately know that it is a proof of the cardinality of the set of prime numbers, for example.

Re: Why Don't People Use Formal Methods?

#189

Post by marcosdumay » Tue, Jan 22, 2019, 2:16 PM UTC

pytester wrote: post #123

cryptica wrote: post #93

Earlier quoted context omitted.

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

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.

Re: Why Don't People Use Formal Methods?

#190

Post by marcosdumay » Tue, Jan 22, 2019, 2:26 PM UTC

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…

Computer science is a branch of mathematics, so proofs are of the mathematics kind.

Formal proofs will prove whatever you designed them to prove. It may be that #1 of yours, or the #2 if you actually know what you want (AKA "never"). Your #3 is mathematically ill defined, and math can not prove ill defined statements.

> When I see people getting excited that they have prooven tail has types [a] -> [a], all I can think of is that some programmer will make "a" some sort of super object at the root of an object hierarchy, and then what on earth is being gained?

I don't really understand that question. The type means that whatever list you pass that tail function, you'll get a list of the same type back. That's information you can decide to use to build your program, or just ignore. Without further context, there isn't any defined value for that information.