undefined | Better HN

0 pointsstiff12y ago0 comments

I can't agree with this either. Practical engineering is not pure mathematics, and once systems get complex enough, even if they are man-designed and not given from nature, there is often no other way than to use "reverse engineering" or in other words use empirical methods to understand some behaviour or fix a problem.

In fact, one of the most important skills to learn for prospective computer programmers is rigorous design of experiments to confirm or deny a given thesis about some aspect of a given system. When you are dealing with a virtual machine on top of an operating system, communicating over a network through tcp/ip with another virtual machine, there are millions of lines of source code involved, not to mention potential hardware issues, how can anyone be expected to understand all of it? Even if some of this complexity is accidental, as soon as we get rid of it we will just build more sophisticated systems, so people will regardless have to know how to deal with systems that do not fit in ones head all at once and where you can't always just reason your way out.

0 comments

4 comments · 2 top-level

nightski12y ago· 2 in thread

Whoa, you jumped to some conclusions at the end there that just don't add up. Since how is formalizing something counterproductive to building sophisticated systems?

The systems you mentioned were actually built in a non-formalized matter (further emphasizing the OP if anything). Of course it is incredibly difficult to build even more sophisticated systems on top of these systems for that very reason. Many of them are needlessly complicated leaky abstractions - but persist due to industry inertia.

The methods you describe are exactly the problem causing this.

stiffOP12y ago

You are misunderstanding and/or misrepresenting my point, which is that once enough people over a long-enough period build systems in a top-down, systematic matter, well as it works, it becomes impossible for a single person to understand a specific issue about a stack of such systems, especially once the real-world kicks in with hardware issues, bugs, and so forth, in which case you have to resort to methods that do not require keeping all relevant aspects in the head and that do not rely on the truth of idealized assumptions. Like in going from mathematics to physics, in real-world software engineering is no longer sufficient for conclusions to follow logically from the premises, since the premises now also have to be true in the real world conditions. Having non-leaky abstractions only shifts the moment in which the shift from pure thought to empiricism has to happen.

It seems to me that you actually use the notion of being "formal" in an informal (sic) way. Remember we are talking about Dijkstra-style correctness proofs and developing programs via doing mechanical in nature transformations of program invariants.

nightski12y ago

I am not convinced that in order to use the methods described one would have to keep the entire "world" in their head. In fact, I think these methods would actually help manage that problem rather than exacerbate it.

In the end a software program is and always will be an approximation of the real world.

loup-vaillant12y ago

Complexity is not hopeless.

First, http://www.vpri.org/html/work/ifnct.htm and http://www.vpri.org/pdf/tr2011004_steps11.pdf (Personal computing, which currently fit in about 200 Million lines, or 10 thousand books, could actually fit in about 20.000 lines, or a single book.)

Second, as we make more complex systems, we could just prove that they work as intended. (Provided the underlying hardware works as intended, which as you pointed out is not allways the case). Okay, it's expensive to prove your software. But it's not impossible: just use proven libraries, and prove that your software works if the dependencies and the hardware work. No need to prove the whole stack.

Sure, it's expensive in the short term. But think of the total absence of effort you will need to invest over debugging.

---

Of course, right now, we're deep in the poo. Hail to Worse Sells Better!

j / k navigate · click thread line to collapse