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

81–90 of 232 posts

Re: Why Don't People Use Formal Methods?

#81

Post by throwawayjava »

TeMPOraL wrote: post #76
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…

I'm not buying it; I believe the problem is more on the human side. "Most applications are being specified by people who don't understand in any detail what they want the application to do", because most humans absolutely suck at clear communication and clear thinking. They're not aware what they're not communicating. They're not aware what scenarios they're not considering. Examples abound - remember that time where…

You and twic make similar points, which I think are reasonable but miss a very fundamental difference between e.g., ecommerce webapps and something like a robot.

The how and what questions in robotics/manufacturing ground out in formal methods style mathematical modeling in a way that the sort of questions that dominated the last couple cycles of tech did not (because those tended to be behavioral specifications about humans -- click more ads, book more taxis, click the buy button, etc).

Formal methods didn't capture "engagement" or "click-through rate", but they do capture "safety" and "liveness".

Consider any of the examples you give. At the top level of the design process, we need to derisk things that demand mathematical modeling (battery life, car behavior). How do you go about determining the probability of a car colliding, or tease out the various things that might inform that probability? Not (only) by white boarding with business stakeholders or asking consumers, but (also) by building models of how the system behaves and analyzing those models.

Obviously, formal methods aren't a silver bullet, and yes, software engineers will always spend a lot of time at whiteboards and in meetings.

But when it comes to the future of formal methods, the question is whether the systems we expect to take center stage in the software world look like to sorts of systems where properties like "safety" and "liveness" are a) hard to specify, b) lend themselves to mathematical analysis, and c) are critical to business success.

I think the answer to that question is yes.

Re: Why Don't People Use Formal Methods?

#82

Post by ghayes »

For me, working on contracts on Ethereum, I have found formal methods to be invaluable (we use a tool by Certora [0] based on CVC4 solver). The trade-off shifts once you enter the world of immutable code, and the time we've spent designing, reviewing and now formally testing has been invaluable to shipping our product with confidence. We tend to think of our formal specifications like the ultimate unit test (instead of testing a few cases, test every possible case). Also, the prover has found subtle bugs which have really put a smile on my face.

An example spec might look like this:

    description "Admin (and only admin) can set new admin" {
      // e0, e1 can hold any possible environment and are ordered sequentially
      env e0; env e1;

      // free variable for possible values of new admin
      address nextAdmin;
      havoc nextAdmin;
  
      // call to set the new admin
      invoke setAdmin(e0, nextAdmin);

      // assert one of two conditionals must hold for all cases:
      // 1. We were the admin and the next admin is what we sent to `setAdmin()`
      // or 2. We were not the admin, and the next admin is whatever is was before our call to `setAdmin()`.
      static_assert (
        e0.sender == invoke admin(e0) &&
        invoke admin(e1) == nextAdmin
      ) || (
        e0.sender != invoke admin(e0) &&
        invoke admin(e1) == invoke admin(e0)
      );
    }
It's a few lines of code to verify a simple function, but it's incredibly powerful for us to know that our code works in all cases.

[0] http://www.certora.com/

Re: Why Don't People Use Formal Methods?

#83

Post by perlgeek »

joe_the_user wrote: post #21
empath75 wrote: post #8

Earlier quoted context omitted.

Unlike the case of building an airplane, when you’re developing software you don’t know when you start sometimes if you want to build an airplane or a helicopter, or even if you want to fly, or indeed, if you’re building a vehicle of any kind, and not some kind of corn mill or a movie theater, perhaps.

The thing about software, indeed, most of it isn't space shuttles or life support systems. But it can go from paper airplanes to model airplanes to real airplanes more quickly than you'd think. Your hobby website could take-off to be an income and then a company and have leftover code all around.

> But it can go from paper airplanes to model airplanes to real airplanes more quickly than you'd think.

It seldom does.

> Your hobby website could take-off to be an income and then a company and have leftover code all around.

When it provides you with an income, you can justify spending more time on refactoring, tests and correctness.

Re: Why Don't People Use Formal Methods?

#84

Post by DoctorOetker »

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

Re: Why Don't People Use Formal Methods?

#85

Post by goto11 »

Formal methods assume the difficult part of software development is producing code which precisely conforms to a specification. In reality the difficult part is to even get to an unambiguous specification with represent the actual business needs, which are often vague or unknown when development begins.

This lead to iterative development. But iterative development does not go well with formal methods. With vague specs and iterative development, the code itself ends up being the spec. If well-written, the code even reads like a spec, and during the iterative verification, it is proven if the spec/code conforms to the product owners actual (often unstated) requirements. Just take user interface design: It is incredible hard to design a good GUI for a complex application and requires multiple rounds of user testing and refinements. But if you actually have a spec for an UI, implementing it is trivial and can be done by the intern.

More fundamentally: If you do have the spec stated completely and unambiguous in a formal language...why don't you just compile the spec then? Seriously, why translate it by hand into a different language and then spend a lot of effort to prove you didn't make any mistakes in this translation? DSL's and declarative languages seem more promising as ways to bridge the gap between spec and code.

That said, there are obviously domains where formal methods are worth it, because you really want the extra verification in having the logic stated twice. Especially in hardware development which doesn't lend itself to iterative. It is just a small part of software development overall.

The most promising future for formal methods are in type system, since they are not separate from the code, so they lend them selves much better to refactoring.

Re: Why Don't People Use Formal Methods?

#86

Post by agumonkey »

kod wrote: post #79
mikekchar wrote: post #63

Earlier quoted context omitted.

Strong type systems with type inference are new(ish) for a guy as old as me :-D

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

Re: Why Don't People Use Formal Methods?

#87

Post by hvidgaard »

kod wrote: post #79
mikekchar wrote: post #63

Earlier quoted context omitted.

Strong type systems with type inference are new(ish) for a guy as old as me :-D

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

It's even older than that. The Hindley–Milner type system was first described in 1969. In other words, we've had the foundation for this kind of type inference for 50 years.

Re: Why Don't People Use Formal Methods?

#88

Post by ddingus »

kod wrote: post #79
mikekchar wrote: post #63

Earlier quoted context omitted.

Strong type systems with type inference are new(ish) for a guy as old as me :-D

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

What's the deal?

Really could be new to him. It's a pretty big world out there.

Re: Why Don't People Use Formal Methods?

#89

Post by baby »

ghayes wrote: post #82

For me, working on contracts on Ethereum, I have found formal methods to be invaluable (we use a tool by Certora [0] based on CVC4 solver). The trade-off shifts once you enter the world of immutable code, and the time we've spent designing, reviewing and now formally testing has been invaluable to shipping our product with confidence. We tend to think of our formal specifications like the ultimate unit test (instead…

Formal verification totally makes sense for smart contracts as they are relatively small most of the time (around 500 LOC). When your program is tied to so much money, this is probably what you should be doing.

Re: Why Don't People Use Formal Methods?

#90

Post by josh2600 »

ghayes wrote: post #82

For me, working on contracts on Ethereum, I have found formal methods to be invaluable (we use a tool by Certora [0] based on CVC4 solver). The trade-off shifts once you enter the world of immutable code, and the time we've spent designing, reviewing and now formally testing has been invaluable to shipping our product with confidence. We tend to think of our formal specifications like the ultimate unit test (instead…

This makes sense, but I still think it’s really hard to formally verify immutable code against a mutable VM.

Your code can be correct today but the VM can change tomorrow.

Post reply on HN