undefined | Better HN

0 pointsChris_Newton10y ago0 comments

It happens that writing something nontrivial that works in the real world requires all the details, checks and abstractions it contains.

I think it helps to separate essential complexity, due to the nature of the problem you’re trying to solve, from accidental complexity, which comes from other sources. In an ideal world, you’d represent the essential complexity as clearly and flexibly as possible, and minimise the amount of accidental complexity you put on top.

That accidental complexity can come from lots of different sources: tools that aren’t a perfect fit for what you’re trying to do, a design that isn’t as clean as it could be, an unfortunate choice of data structures of algorithms… I suspect it probably is fair to say that a lot of accidental complexity that goes into real world programs could have been avoided if, for example, more appropriate tools had been used or better design decisions had been made during development.

0 comments

6 comments · 2 top-level

twa92710y ago· 3 in thread

I claim that the essential complexity of real world software is inherently high. Yes, the accidental complexity can balloon to infinity (FizzBuzzEnterpriseEdition), but even the simplest possible software solving a given real world problem will be always highly complex.

This is why mathematical proofs of software correctness are impossible in practice. A small 100-200 LOC program takes a qualified mathematician weeks to create a proof of correctness. No particular step of a program is complex, but it combines a lot of these simple steps.

Chris_NewtonOP10y ago

I claim that the essential complexity of real world software is inherently high.

Sometimes it certainly is high, but why inherently? Surely it depends on the particular problem you are interested in solving?

This is why mathematical proofs of software correctness are impossible in practice. A small 100-200 LOC program takes a qualified mathematician weeks to create a proof of correctness.

As someone who actually does formally prove things about algorithms significantly larger than that from to time, I believe you’re exaggerating here.

See the CompCert C compiler[1] for an example of using formal proofs in real world programming at a much larger scale.

No particular step of a program is complex, but it combines a lot of these simple steps.

And this leads to the “secret” of being able to construct proofs for realistic programs in useful amounts of time, in my experience: you have to be able to decompose the fundamental problem into manageable parts, prove some properties of interest for those parts, and then be able to compose the things you’ve proved separately in order to prove useful things about the overall system. We do this all the time with some properties in strong, static type systems, for example.

[1] http://compcert.inria.fr/compcert-C.html

twa92710y ago

> Sometimes it certainly is high, but why inherently? Surely it depends on the particular problem you are interested in solving?

Even the simplest "real world" programs do things like: communication with a database, string manipulation, calling library functions which can fail.

> As someone who actually does formally prove things about algorithms significantly larger than that from to time, I believe you’re exaggerating here.

I wrote a master's thesis that touched the subject and it's what I put in an introduction as an illustration of the field's difficulty (I believe it was not taken from air ;). I don't know the field now but ca. 10 years ago program's proofs were mainly refinements of high level axioms to executable code so there was no separate "proof" step of a finished program, but still the added complexity of proving the refinement steps was huge.

1 more reply

sdboyer10y ago

> and then be able to compose the things you’ve proved separately

This has always struck me as the really challenging, problematic part about correctness proofs. I've no formal training in this area (sadly), but how does one go about being able to just compose your proof components? Often as not, that seems like a pipe dream - http://queue.acm.org/detail.cfm?id=2889274

Avshalom10y ago· 1 in thread

The problem is that when people get told to cut a board to 1 meter and we get handed a .5 meter board we say "fuck you" the program on the other hand needs to be explicitly told how/when to say fuck you, and it needs that for basically every single possible source of error.

That doesn't fit into either of your categories really but it's where so much of the actual complexity comes from.

raould4210y ago

I for one applaud your use of the vulgar and am doing my best to upvote you mightily.

j / k navigate · click thread line to collapse