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

221–230 of 232 posts

Re: Why Don't People Use Formal Methods?

#221

Post by 01100011 »

jen729w wrote: post #100
01100011 wrote: post #92

I love the concept of formal methods. As someone who pushes for more determinism in software(yay state machines), I have long dreamed of using them to prove correctness. And then I go look at the goofy, domain-specific language I'd have to learn, roll my eyes, and get back to doing 'real work'. Formal methods will win when I can point the tools at a mess of C/C++/whatever code and have the tool figure out the rest wi…

I found this quote a while ago while researching state machines. The author is using a moderately complex hypothetical system as a reason not to use a state machine. “... For instance, you are asked to create an online order system. To do that you need to think about all the possible states of the system, such as how it behaves when a customer places an order, what happens if it is not found on stock or if the custom…

Well, state explosion is a real thing, which is why we have things like hierarchical state machines. There's almost always a trade off between capturing everything in a state variable and allowing a few flags and conditionals. The classic example is a keyboard state machine where you don't actually have states for each key pressed, you just store the key in a variable.

Re: Why Don't People Use Formal Methods?

#222

Post by nickpsecurity »

Jtsummers wrote: post #29
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…

Formal methods make sense when you focus them on the right part of your system. Even if it's changing week-to-week, there's an underlying structure or design that's staying consistent. You wouldn't use formal methods on, say, the GUI layout of your system. But you could use it to prove that you're accessing your database in a way that won't cause corrupted or incorrect data to appear. If you're working on anything wi…

"You wouldn't use formal methods on, say, the GUI layout of your system."

That's actually a good use. Statecharts were one method used for formally specifying that. The research I saw would formally specify the individual components or modes, the transitions with their conditions, these would be checked formally, and then maybe some code is generated that's correct by construction. Example for prototyping:

https://sketch.systems/

Re: Why Don't People Use Formal Methods?

#224

Post by anentropic »

pron wrote: post #197
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.

I find TLA+ syntax and tooling to be far better than that of almost all programming languages. E.g., here's a TLA+ spec I recently wrote: https://pron.github.io/files/TicTacToe.pdf The syntax is as close to standard informal mathematical notation as formality can afford.

> The syntax is as close to standard informal mathematical notation as formality can afford.

which is not very helpful to the average non-academic software engineer

Re: Why Don't People Use Formal Methods?

#225

Post by pron »

anentropic wrote: post #224
pron wrote: post #197

Earlier quoted context omitted.

I find TLA+ syntax and tooling to be far better than that of almost all programming languages. E.g., here's a TLA+ spec I recently wrote: https://pron.github.io/files/TicTacToe.pdf The syntax is as close to standard informal mathematical notation as formality can afford.

> The syntax is as close to standard informal mathematical notation as formality can afford. which is not very helpful to the average non-academic software engineer

The entire language is based on specifying using simple mathematics (little more than high-school level), so this is the appropriate notation; a more programming-language like notation would be confusing as TLA+ is not programming. Those who have not learned basic maths notation in college can learn it in an hour (and automatically learn how to read maths in the process). The language is much simpler than Python. The entire language (except the proof language, which most people won't use at all) including all of the "standard library" is described in just a few pages: https://lamport.azurewebsites.net/tla/summary-standalone.pdf

Re: Why Don't People Use Formal Methods?

#226

Post by pron »

nextos wrote: post #209
pron wrote: post #158

Earlier quoted context omitted.

I think you're mistaking the use of formal methods for some particular process (like confusing tests with TDD). Formal methods do not require that you have a specification in advance. They can help you come up with the specification, through interaction, before or during coding (e.g., this is a lightweight formal specification tool for designing UIs and interaction: https://sketch.systems/ ). As code is itself a spec…

I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost anyone here. Formal methods still lack a bit of maturity and streamlining to get adopted. It's a bit like functional programming in the late 90s and early 2000s. Nothing was terribly different from now, yet it was not widely used. Whereas now, we are starting to…

Judging by the reading list you've provided below, you may not be familiar with more "productized" formal methods, designed for use by working engineers, like TLA+ and Alloy. I don't know if I'd call them entirely "mature" yet, but they are certainly industrial-strength, learned by ordinary programmers in 2-3 weeks of part-time reading of tutorials or in a few days with guidance, after which they go on to specify and verify large, complex real-world systems.

Lamport spent years simplifying TLA+ and designing it for user-friendliness (at the cost of making it inappropriate for logicians to do research on novel logics). While extremely powerful (people have implemented TLA in Isabelle and Coq to reason about concurrent and interactive systems), it is based mostly on ordinary, high-school or first-year-college math, and entirely eschews the complications of programming language semantics.

See the following industry reports:

* Amazon: http://lamport.azurewebsites.net/tla/formal-methods-amazon.p... -- this has been so successful that managers encourage developers to use TLA+ to reduce development costs.

* Microsoft: https://youtu.be/ifFfxRCX_jw

* https://youtu.be/tfnldxWlOhM

Re: Why Don't People Use Formal Methods?

#227

Post by mitchtbaum »

It's also a lot easier to do change management on an abstract model of the software you're working on than the design of that one program itself, because the design choices made by other sister programs can be immensely helpful. It's the inversion of making decisions in a vacuum. What do you call that?

---

Edit for "random" keywords: model-driven engineering with domain-specific meta-modelling languages

Re: Why Don't People Use Formal Methods?

#228

Post by zzzcpan »

luord wrote: post #210

> In fact, the vast majority of distributed systems outages could have been prevented by slightly-more-comprehensive testing. And that’s just more comprehensive unit testing, Key takeaway for me as far as code verification goes. Design verification reminded me of a few subjects I studied in college.

Take that claim with a grain of salt. More comprehensive testing still requires deep expertise in resilience/reliability to even just understand what to test for. And you can't have that unless you both study that domain and experience first hand the sheer amount of problems such systems have in the wild.

For example, you might assume there is no difference if you establish TCP connection to a port 12345 or to a port 12346 of the same server. But there is, they might belong to different buckets in a network stack somewhere and one bucket might have too many packets in it and be slow and overloaded, while another isn't and be perfectly fast. This could easily cause outages. Distributed systems are strange like that.

Re: Why Don't People Use Formal Methods?

#229

Post by awwx »

agentultra wrote: post #198

To counter the exhaustive number of comments about how expensive, impenetrable, and unrealistic formal methods are in practice: I have been using formal methods in my work . To borrow the parlance of the author, I use TLA+ -- a design verification tool -- in my work. Some of my work is in lightly regulated food and drug industries but most of it is not. It hasn't cost my company a tonne of money or delayed projects.…

> Some features in our products use an event sourcing pattern

Ah, sounds very interesting!

Are there any examples you'd be able to share?

E.g. one example of a TLA+ assertion that your event store is serializable, or whatever you can?

Re: Why Don't People Use Formal Methods?

#230

Post by UncleMeat »

achamayou wrote: post #214
UncleMeat wrote: post #202

Earlier quoted context omitted.

There are papers that use SMT over RNNs to prove smoothness of the output functions. You can absolutely apply these techniques to ML.

So you have any links? I’m very curious, and a quick search did not turn up anything.

Clark Barrett's group at Stanford (previously NYU) is a leader here.
Post reply on HN