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

191–200 of 232 posts

Re: Why Don't People Use Formal Methods?

#191

Post by phtrivier »

mbrock wrote: post #160
phtrivier wrote: post #121

I might be missing something obvious, but from my (small) reading about TLA+ (and the lamport video course), my biggest concerns were: A: even if you understand the spec you want to write, it's possible to get the implementation of the spec in the spec language wrong (see the Die Hard exercise in the course) ; isn't there some kind of recursive catch-22 there ? B: even if you understand the spec you want to write, an…

There’s a huge misunderstanding that pops up in every discussion about “formal methods.” These methods are not perfect silver bullets to guarantee bug-free software forever. They are supposed to be useful engineering tools that help you think and verify your thinking especially for tricky corner cases and interactions. So then it’s a bit like “Why would I think about the code I’m going to write when I could later mak…

Fair enough.

If you have experience, what would be the rebutal to my fear of the "catch-22" ?

What I mean is, how often does it happen that you think about a problem right, but fail to transcribe that in a formal method, you gives you either too much confidence in a model that does not work, or makes you feel you have wasted your time on mental self-molesting ?

How do you approach "experimenting" with formal methods to avoid this risk ?

Re: Why Don't People Use Formal Methods?

#192

Post by Dirlewanger »

cjensen wrote: post #34

Do people read "The Mythical Man-Month" anymore? The answer to questions like these are part of the book. First, there is no "Silver Bullet" which makes software development easy. Second, adding a layer of additional effort like Formal Methods necessarily either (a) increases development time significantly or (b) exponentially increases headcount. I'm not suggesting that you avoid Formal Methods. It might really fit…

This is a side-effect of receiving a computer science degree and going into a programming job; you'll learn the skills to program, but all the CS theory stuff that you won't use really should have been more practical SE stuff taken from classics like Mythical Man-Month, Design Patterns, etc.

Re: Why Don't People Use Formal Methods?

#193

Post by Retra »

chii wrote: post #179
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…

Or, don't split between primitives vs objects. I think it's a mistake to make thet distinction in many language's design.

The result of that will not be easy to use objects, but hard to use primitives.

Re: Why Don't People Use Formal Methods?

#194

Post by agentultra »

im_down_w_otp wrote: post #47

As a person who does and who's founded a company partially on the basis of the value of them, my opinion is that, in-part, it's because the ecosystem is extremely fractured, the tools are often an esoteric projection of the inside walls of one mad scientist's head turned into software, and they often don't scale very well (mostly due to the two previously mentioned conditions). Additionally, the tools are often desig…

What's your company? I'm interested in the commercial success of these tools and bringing down the cost of using them to industry-acceptable levels so they can be used in more projects.

Re: Why Don't People Use Formal Methods?

#195

Post by hellerup89 »

pron wrote: post #158
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…

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 see adoption by mainstream players. E.g. lots of features in Swift.

With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

Re: Why Don't People Use Formal Methods?

#196

Post by pron »

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…

Do unit tests or type systems make sense when the product changes from week to week? Unit tests and type systems are a formal method (technically; usually they usually do not fall under the academic discipline of formal methods). Formal methods cover a very wide range of tools, that drastically differ in cost and effort. Also, if you have code, then you have a spec, because the code is itself a formal specification. It's just not a very convenient one because it is a very low-level spec.

Re: Why Don't People Use Formal Methods?

#197

Post by pron »

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.

Re: Why Don't People Use Formal Methods?

#198

Post by agentultra »

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. In fact I don't think anyone has really noticed it too much.

Some features in our products use an event sourcing pattern and the architecture is built using a few different components that all need to work in concert. The system can't be validated to be correct with the source code alone. The integration tests can't capture every possible path through the code to ensure we only hit valid, desired states. For those features I maintain a couple of TLA+ specifications in order to ensure our design maintains the properties we desire: we only hit correct states, never drop messages in the face of component failures, that our event store is serializable, etc. And that has informed how I direct the team to design our software implementation.

I don't go to great lengths to validate that our implementation faithfully implements the specification but I do use the TLA+ models to inform the implementation and vice versa: sometimes we discover things during the development process that I use to update my models. One informs the other and it helps me to manage the complexity of those features with confidence.

It doesn't cost us a lot of time or effort for me to do this work. The customer doesn't care at all: they only see the user interface but they do expect their data to be consistent and that failures are not catastrophic. Formal methods have been helpful in this regard for my team.

Edit I started using TLA+ a few years ago to find and resolve bugs in OpenStack; it has been an effective tool and I always recommend learning it.

Re: Why Don't People Use Formal Methods?

#199

Post by mattmoss »

marcosdumay wrote: post #189
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…

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

> That's a problem with specs, the most concise and complete way to write them is by writing your program.

I've never dealt with formal specs/design, certainly nothing like those described here. Your comment (however in/accurate) strikes me as interesting and leads me to wonder...

What if we took the code and processed it to generate a "spec"? (I quote "spec" here b/c I wouldn't consider it a spec, but don't know what else to call it.) Basically, a document that explains verbosely what the written code does... hopefully in a way that is reasonably, humanly digestable.

Then we might get a doc that says, "Function add(...) accepts two integers/nulls and returns the sum." And Joe-coder looks and realizes it shouldn't accept nulls, goes back to the code, fixes the issue.

Re: Why Don't People Use Formal Methods?

#200

Post by agumonkey »

dmitriid wrote: post #159
agumonkey wrote: post #130

Earlier quoted context omitted.

is it published online ?

Found it here: https://stackify.com/whats-new-in-java-10/ ——— start quote ——— This feature has been a long time coming. It was suggested as far back as 2001, and was closed at that time with the following comment by Gilad Bracha: Humans benefit from the redundancy of the type declaration in two ways. First, the redundant type serves as valuable documentation – readers do not have to search for the declaration of getM…

Interesting, I kinda agree about the need for redundancy at times (which is not forbidden by ML typing). But it rejected a very good idea for a decade.. A bit like lambda expressions. Damn Java
Post reply on HN