Hacker News Reader

Comment by drewcoo | Hacker News Reader

I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact.

I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds:

"component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with

"component B just passes requests and routes results, dude, component C is messed up" combined with

"component C never promised that behavior and if you look at our spec it even says so!"

That's an example of your "does not match what was expected" case.

I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.

View on HN

Yes, this!

What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; however, all formal systems I've experienced are not powerful enough to do this at scale in any interesting program, not without spending way more time reconstructing the entire system in the formal world, with the attendant likelihood of introducing spec bugs in that reconstruction.

It is entirely different in the world of hardware, where the specification in many cases is the RTL and the thing being proved is the, supposedly identical, physical implementation.

That's actually what many formal tools excel at. Of course, you have to do have to define "never promised that behavior" which is extra work that nobody wants to do.

Yes. That's "design by contract", which is extremely useful for determining who's at fault.

This came out of aerospace, where it's taken seriously. If A won't interoperate with B, you check the interface spec. If A is out of compliance, A has to be fixed. If B is out of compliance, B has to be fixed. If you can't tell, the interface spec has to be fixed. This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.

This worked in the era when the buyer had more clout than the seller. Now, if A won't interoperate with B, it's the problem of whomever is smaller.

> This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.

Wait wut? Are you talking about their embedded software or the hardware itself? Because if you're talking about the hardware, I'm about to be dumbfounded that there are formal verifications of hardware, my mind is about to be blown.

You could think of many of the formal tools outside of dependently typed programming as design by contract plus a thingy that complains if the contract doesn't work.

This kind of, “Just what the heck in this pile of parts is impacting the other stuff and how is the other stuff impacting this part?” was precisely the angle we took with our V&V tools.

Formal methods have their applications and specific use cases. It all depends on how much is at stake, economically.

I suggest checking into Alloy, which is far easier to work with. It feels like writing a SQL schema, but you get bounded model checking and much more.

formal methods has value in safety related software. When you are developing software for airplane, rail, automobile and nuclear power station, any tools that might improve safety merit consideration.

Reply on news.ycombinator.com