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

211–220 of 232 posts

Re: Why Don't People Use Formal Methods?

#211

Post by pron »

cryptica wrote: post #93
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…

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…

But if you write some code, you must be writing it to do something. That something is your spec. This may or may not be what the customer wanted, but writing it down may make it easier to explain what it is that you've decided to implement, and understand whether or not it could be the right thing.

Requirements do change constantly, which is all the more reason to write specs, so that you can understand the change and its implications (and present it to your customers) before writing the code. I am not saying this is always the best approach, but changing requirements in itself is not a reason not to use formal specification, but an additional motivation to use them.

For example, this is a nice lightweight formal specification tool that allows to specify UI interactions quickly and play with them to see if they are satisfactory before implementing them: https://sketch.systems/ This is more "agile" than changing code between iterations.

Re: Why Don't People Use Formal Methods?

#212

Post by craftinator »

walrus1066 wrote: post #128
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…

Indeed, I've never in my career (in high level businesses, I.e. Finance, advertising) seen such a thing as a proper 'specification'. It's more the business has a high level, rough idea of a change/feature to improve the business, and we figure out together the exact details, some of which surface during implementation, and then verify it gradually in the wild. We could have spent x10 time instead drawing up a formal…

So the people designing the spec don't have enough information about the problem space. As the programmers begin working, they explore the problem space, extract the information they need to understand a solution, and then they can actually solve it. Bit of a Schrodinger's cat situation... The solution must remain undefined until observed.

Re: Why Don't People Use Formal Methods?

#214

Post by achamayou »

UncleMeat wrote: post #202
AstralStorm wrote: post #144

Earlier quoted context omitted.

You can prove the ANN works, but how do you check it conforms to any specification, other than by testing and accepting high probability of real world failure? Eventually, you have a high level fuzzy requirement which is hard to even specify right. Just look at, say, latest YouTube guidelines about content they try to ML around to make tractable... And that's a classifier, now try to do the same with a machine transl…

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.

Re: Why Don't People Use Formal Methods?

#215

Post by ausimian »

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

I learnt and used TLA+ while working at msft, and I'm still using it today:

- anytime I have some protocol or state machine whose behaviour isn't obvious, I write a TLA+ spec. - the process of writing it clarifies my understanding and leads to new insights. These insights directly inform the code and the tests. - the model checker makes it very easy to check sophisticated properties of the algorithm.

I don't use it all the time, but it's a tool I'm very happy I invested in.

Re: Why Don't People Use Formal Methods?

#216

Post by ejcx »

sfrank wrote: post #131
ejcx wrote: post #19

Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B. Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.

That is because the formal method supplement of the DO-178C is RTCA DO-333. There you have about a hundred pages concerned with the application of formal methods.

Good to know. I will buy this doc and give it a read, thanks.

Re: Why Don't People Use Formal Methods?

#217

Post by jlelonm »

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…

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

This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend?

If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragraph executive summary and 10 is an entire Ph.D's worth of training. I'd probably be looking at a 2.5 to a 5.

Re: Why Don't People Use Formal Methods?

#218

Post by magicalhippo »

Tempacc78534 wrote: post #4
jpollock wrote: post #3

I've always wondered how I can write a specification in a language which is complex enough to cover the problem, clear enough to be verified by the customer, and not have it be as complex as writing the code.

The solution is to write partial specs. For example, if your client wants a piece of code which doesn't crash and sends a message over the network. You can write 2 partial specs i.e. 1) it doesn't crash 2) it sends a message over the network. The partial specs can be individually simple but the program which satisfies all of them will be complex. This idea of partial specs follow the general SE design practices as we…

Any message? Or a specific one?

I mean, at my work, a lot of our customers don't even know what our program needs to send to some other program until months after the change needs to be live...

Re: Why Don't People Use Formal Methods?

#219

Post by jacques_chester »

School-Cotton wrote: post #187
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…

Most of what I've seen lately is queueing theory, markov processes or statistics, and yes, I have seen notation used for hundreds of pages at a time and I've seen these symbols used to mean different things (not including partial differential).

One of the books I read recently[0] has a table of where symbols and formulae are first defined. It's a godsend.

But I would prefer self-describing names to a lookup table. I don't put comments at the top of each file of code with such a table.

[0] https://highered.mheducation.com/sites/0073401323/informatio...

Re: Why Don't People Use Formal Methods?

#220

Post by nextos »

jlelonm wrote: post #217
nextos wrote: post #209

Earlier quoted context omitted.

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…

> 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. This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend? If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragr…

Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background):

* Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/

* Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/

* FRAP (Chlipala): http://adam.chlipala.net/frap/

* Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking

* Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100

* Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/

Post reply on HN