Hacker News Reader

Comment by miceeatnicerice | Hacker News Reader

No software is creatively fathomed out of nothing. Opinionated frameworks abound, pre-ordaining the little manouevres needed to wire them up properly, and solving familiar problems with established patterns. If these have all been decided beforehand, even if only by convention, then what are they but blueprints?

What difference there is works in software's favour: there's a frothy top layer of most projects where developers can indulge their whims/hone their abilities and approaches. But it's not the whole.

View on HN

Physical items are built the same way; everything is built from smaller components many of which are farmed out to other providers. When you have a blueprint for a bridge you don't also plan the forging of the bolts.

The parts you're talking about (in either software or bridges) are important but aren't where the design effort goes. Everything interesting in every project is in that frothy top layer.

They aren't blueprints, they're foundations and components if we're going to stick to this analogy.

Blueprints are specifications and design documents. Most software lacks these.

Specifications and design documents are merely estimations. If you've made every single decision possible, you've written the software.

If you have blueprints for a bridge and get two different companies to build it, you'll get the same bridge both times. The differences, if any, would be minor.

If you give specifications and design documents to two software teams you could get radically different products that look nothing alike and it's entirely possible that neither one of them will satisfy the clients needs.

If they don't meet the clients needs then they were the wrong spec and design document.

Honest question: without a specification, how do you verify your software?

There is plenty of software that is driven entirely by specification. Inputs come in and outputs go out. And you validate that with a test suite, etc.

But even more software is designed not for machine-machine communication but for machine-human interaction. And humans are notoriously bad at knowing what they want and need. In some cases, the existence of software so fundamentally changes the nature of work that humans don't even have the frame of reference necessary to provide full specifications. Yet the software still has to be written, do it's job, and be accepted. I'm not sure I have an answer to your question but somehow I still get the job done.

Given a formal model or proof of a system and the two teams will either succeed or fail.

Give them a specification in prose and they will have a little too much wiggle room. Such specifications are useful to a degree but I look at them like sketches on a napkin.

If you use a more formal method of mathematics as your specification then you can be more precise about the invariants that matter and model your system more faithfully. And with a good proof assistant or model checker the computer can even help you catch flaws in your design that you would never have been able to think of on your own.

It's true that the source code is a proof of something. It often helps to know whether you've built the right thing. And that it does what you think it does.

Given a sufficient model or proof of the system and you don't need the teams at all -- they can be automated away.

Getting your model right is as hard, if not harder, than getting the software right in the first place. The problem hasn't changed you've just added more layers (and more cost) in the hopes that doing it twice, differently, eliminates most of the problems.

For some trivial small problems writing a model in TLA+ or Lean is definitely more costly than just writing the software even if you get a few things wrong. It'd be like commissioning a blueprint for your shed in the backyard. For those sorts of tasks it is sufficient to just write a few tests and call it a day.

However for more complex services that are trying to manage several clusters of resources amongst tens of thousands of tenants or more there are invariably going to be errors. The kinds of errors you see might require a particular series of events to change your state in 53 steps to hit it... but if you're servicing > 1M requests in a minute that ends up being frequent enough to be bothersome.

Even more so if you're working on a memory controller in a new hardware platform that is expected to ship in a few million units. It'd be nice to know that you have strong evidence that your system is correct.

And developing models is hard but so is thinking. Nobody said it was easy. But one shouldn't say that we can't engineer robust software systems. It's just patently false.

Reply on news.ycombinator.com