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

141–150 of 232 posts

Re: Why Don't People Use Formal Methods?

#141

Post by fmap »

roenxi wrote: post #115
Symbiote wrote: post #111

Earlier quoted context omitted.

Proof in formal methods means the mathematical kind: with certainty the program / function implements the specification. Mathematicians can also prove something irrelevant or useless, or something fundamental like 1+1=2.

Well, yes, but if mathematicians prove something then we know it is true. And if they can't prove the trivialities, that would be a crisis for the entire discipline, because 1+1=2 relates to everything they do. If software people prove something we also know it is true, but not that it usefully relates to the software. In fact, 0.1+0.2 is likely != 0.3 for most software. You can prove you have integer types or fracti…

> So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing?

Empirically, yes it is (see e.g. "Finding and understanding bugs in C compilers"). Testing can show the presence of bugs, proofs show the absence of (a class of) bugs. This is a worthwhile exercise, even if your model is not perfect.

This is not an all-or-nothing proposition. There are lightweight forms of formal specification and proofs which you are probably already using. One example are types. If your program is well-typed it might still crash with a division by zero or some other runtime error, but it will not crash because you tried to execute code at address 42 after you mixed up your integers and code pointers.

Re: Why Don't People Use Formal Methods?

#142

Post by edpichler »

Since I started designed before code I am at least 2x more productive, rework was reduced to almost zero. Anyway, it is difficult for us to understand things really abstractly, and to measure the future gain of not so fun activities.

Re: Why Don't People Use Formal Methods?

#144

Post by AstralStorm »

throwawayjava wrote: post #105
achamayou wrote: post #71

Earlier quoted context omitted.

As a counterpoint to that, another change happening in the industry now is the increasing tendency to delegate more and more to ML models, which are even less amenable to formal verification than mainstream PLs.

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

Re: Why Don't People Use Formal Methods?

#145

Post by danpalmer »

TheFattestNinja wrote: post #140
tanilama wrote: post #129

If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…

Can you give me more examples of FM used in finance? I feel like they should be used, but in my limited experience with finance-related gigs I've been aghast at the lack of even basic testing put in place...

From what I've seen, most finance development seems to be "work hard not smart" – throw a lot of developers with a wide range of skill, poor development workflows, and QA at a problem, and then back them up with shifting the liability to someone else. This mostly works, it just costs a fortune and results in moving very slowly.

Re: Why Don't People Use Formal Methods?

#146

Post by patates »

TheFattestNinja wrote: post #140
tanilama wrote: post #129

If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…

Can you give me more examples of FM used in finance? I feel like they should be used, but in my limited experience with finance-related gigs I've been aghast at the lack of even basic testing put in place...

It depends on the stakes mainly, but also the experience of the stakeholders of a project. Both extremes (heavily tested, proven code vs "let's hope this works" code) are common but usually you're not allowed to speak about anything because of non-disclosure agreements and proven or not, all code is manually tested like crazy anyway. You commonly get insane overhead and just working code.

Re: Why Don't People Use Formal Methods?

#147

Post by patates »

pasta wrote: post #138
tanilama wrote: post #129

If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…

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…

Ada has subtypes for such cases: https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Co...

Re: Why Don't People Use Formal Methods?

#148

Post by AstralStorm »

logicchains wrote: post #127
TeMPOraL wrote: post #77

Earlier quoted context omitted.

At GP's level of specification, things shouldn't change even then, unless you're doing an actual redefinition of what the software does and why. Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document".

>Even if a new feature is cutting across all layers in your code, it's unlikely that it'll alter the requirements like "parallel edits don't corrupt the document". What if you're building MongoDB a decade ago, and the new feature is "perform faster on benchmarks"?

That is not a properly specified or useful requirement.

1) Your benchmarks have to be validated to correspond to real life usage. Especially problem sizes and specific structure. (Whether collisions are needed, what kind of queries etc.)

2) A proper performance specification is WCET or runtime histogram for given piece of code, which can be checked with a model checker.

3) It is a requirement to pass a given test "better". If that sounds good to your clients, well, you're selling a database to clueless people who somehow care about a specific benchmark... Competitors will pick a different benchmark to brag about.

4) Problematic parts of the code have to be identified, specified and fixed. And tested. If you do not match performance spec by then you have a different problem and need to redesign the software including algorithms used most likely. Very expensive.

Re: Why Don't People Use Formal Methods?

#149

Post by fmap »

> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification

I suspect that most bugs are introduced because programmers do not have a clear idea of what their code is supposed to do. There are simply too many levels to keep track of at the same time. E.g., in C you are manually keeping track of resource ownership and data representation at the low-level, while at the same time keeping the overarching architecture present in your head. The latter typically has several moving pieces (different threads, processes, machines) and keeping a clear picture of all possible interactions is a nightmare.

Formal specifications can help with this, by first specifying the full system and then deriving precise local (i.e. modular) specifications. In my experience, programming is typically easy once I have a problem broken down into isolated pieces with clear requirements. It's just that most systems are so large that getting to this point takes serious effort.

Here you run into a cultural problem. You need to convince people to put effort into something that they do not implicitly regard as valuable. It makes sense to me that people aren't using formal methods, unless there is very little friction when getting started.

Re: Why Don't People Use Formal Methods?

#150

Post by TuringTest »

agumonkey wrote: post #130
dmitriid wrote: post #117

Earlier quoted context omitted.

> Probably rejected willingly even ('where are my objects?') Local type inference was rejected in Java in 2001 because "you need to spec your types precisely"

is it published online ?

IIRC it was common knowledge, as it was an "obvious improvement" over C-style undeclared variables. Have in mind that type inference applied only to local values, not propagated globally through the code structure as in ML.
Post reply on HN