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

201–210 of 232 posts

Re: Why Don't People Use Formal Methods?

#201

Post by philipodonnell »

mattmoss wrote: post #199
marcosdumay wrote: post #189

Earlier quoted context omitted.

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

If there was a rule that functions could only return named variables (vs expressions that evaluate to a value that is returned) it would get closer to "this function accepts paramName1 and paramName2 and returns sumOfParams".

Re: Why Don't People Use Formal Methods?

#202

Post by UncleMeat »

AstralStorm wrote: post #144
throwawayjava wrote: post #105

Earlier quoted context omitted.

Absolutely, but why would that preclude formal methods?! In fact, this is exactly what I was thinking about when writing the last paragraph of my comment.

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.

Re: Why Don't People Use Formal Methods?

#204

Post by UncleMeat »

josh2600 wrote: post #90
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.

This is like the quote about getting the right answer if you put in the wrong inputs.

Of course if you change the program semantics then the program changes. This is a limitation of literally all techniques, including testing.

Re: Why Don't People Use Formal Methods?

#205

Post by radlad »

mattmoss wrote: post #199
marcosdumay wrote: post #189

Earlier quoted context omitted.

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

This is essentially what static code analysis attempts to do. Unfortunately, there are many ways of writing programs that today's static code analysis cannot understand.

Re: Why Don't People Use Formal Methods?

#206

Post by im_down_w_otp »

agentultra wrote: post #194
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.

Auxon Corporation (https://www.auxon.io/ a placeholder site, obviously. Low priority). Founded late last year. We're working on tools and technology for enabling people to build, automatically validate, and verify life-critical automation (e.g. highly-automated driving systems, industrial automation, etc.). But the ultimate goal is broad application.

Currently we work primarily with AV companies, automotive OEMs, and partners in their respective supply-chains. Our ambition is to create for Software & AI Engineers the kinds of sophisticated, accessible CAE tools & capabilities that have been enjoyed by Mechanical & Electrical Engineers for years. Software Engineers have done a phenomenal job enabling other disciplines, but we've done a less compelling job enabling ourselves in similar ways.

Re: Why Don't People Use Formal Methods?

#208

Post by chriscaruso »

"Before we prove our code is correct, we need to know what is 'correct'. This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the spec"

What's the difference between the specification and code at that point? If it's that detail oriented, then isn't the chance of bugs in the specification at least as likely as being in code?

Re: Why Don't People Use Formal Methods?

#209

Post by nextos »

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?

#210

Post by luord »

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

Post reply on HN