Andrew Birkett's blog

I’ve read a lot of engineering history books in my time, but rarely have they evoked Mills & Boon so strongly as this gem:

“He realized a machine to draw the wire from the reel, cut and shape it, pierce the holes in the leather, and place the staples in the sheet; but the forming of the second and final bend in the teeth was a problem that vexed his very soul as one of insurmountable difficulty. Hope was followed by despair, and the most glorious prize of all that would crown his machine with perfection, hovered around him like a phantom, enticing him on to further exertion, yet eluding his grasp. He did not lack, however, the support of encouraging friends, who believed in his ultimate success if he would only persevere believingly and courageously. To the cheerful assurances of his friends may be attributed much of his resolution and unremitting ardor in forcing his scheme to a successful finality.

While in this maze of doubt, his brain hot with feverish uncertainty, his thoughts dwelling vaguely on a theory of possibilities, his exhausted strength permitted the solution to come to him in a dream. Such is the testimony of some, and, whether it be true or not, it is not outside a common experience of many, to retire at night with a mind confused and mystified by unabated application to a single idea, and wake up in the morning with it fresh and clear with the mystery revealed and elucidated, as if it were the work of a vision. He arose at early dawn with a heart full of emotion, and a face beaming with joy, and eagerly sought his workshop to place on his machine the last piece of mechanism that was to transform it into a magnificent consummation”

(from the 1885 book, History of the American card-clothing industry)

“If you try to improve the performance of a system of people, machines, and procedures by setting numerical goals for the improvement of individual parts of the system, the system will defeat your efforts and you will pay a price where you least expect it.”. – Myron Tribus

Myron Tribus was the source of the anecdote about why Shannon chose to name his measure of information after the thermodynamic concept of entropy. Furthermore, Shannon expressed to him “.. misgivings about using his definition of entropy for applications beyond communication channels”.

I don’t know if Shannon knew much about thermodynamics or not – he was an engineer and mathematician. I also don’t know whether Von Neumann (who certainly did know physics) suggested the name “entropy” based only on the superficial syntactic similarity between Shannon’s sum(pi log(pi)) and Boltzmann’s -Nk sum(pi log(pi)) .. or whether perhaps he grokked a deeper connection like what ET Jaynes later tried to pursue.

I bought a 16GB Kindle Fire recently. It certainly works as advertised – nice screen, hdmi out, good onboard sound. But the whole ‘cloud content’ world doesn’t actually fit well with my family world.

The Kindle Fire must be registered to one, and only one, Amazon account at a time. There’s no concept of it being a multi-user device. If it’s registered to me, anyone else using it will get ‘my’ view of the internet .. my browsing history, my books, my recommendations. We actually registered our Kindle Fire to my other half’s account, which leads to the next problem.

In years gone by, we had a pile of CDs which anyone in the family could pick up and listen to. Then when I ripped them all into iTunes, we could still all access them via Sharing. But now, in the glorious cloud future, I’ve imported all my music into Amazon’s cloud player under my account and paid £22 for the year (it’s cheaper than having mp3s backed up in s3). Nobody else in my family can listen to the cloudplayer music except for me, unless I tell everyone my Amazon login details (violating the ToS). Furthermore, I can’t use our Kindle Fire to listen to my, I mean our, music .. because it’s registered to my other half’s account.

Photo sharing is done via Amazon’s cloud drive. Again, that’s a per-account thing. My family has ‘our’ photographs which everyone wants to look at. Photo albums used to sit on shelfs, for anyone to look at. Now ‘our’ photos are silo’d into an individual’s cloud account.

So, all in all, it’s a bit of a mess. Does the ‘cloud content’ world assume that we’re all single 20-somethings living silo’d lives? What about all these cases where “my stuff” is actually “our stuff”?

I bought a textbook on fluid mechanics recently, having a rough plan to learn more about weather patterns by writing a simulation. Expecting a theoretical physics text, I was a bit unsettled to read the following on the first page of the introduction:

“The theory is often frustrating”

“viscocity .. gives rise, at frustratingly small velocities .. to turbulence”

“The theory of turbulent flow is crude .. yet it can be quite serviceable as an engineering estimate”

Crude? Frustrating? “Engineering estimate”? These are not words I’ve ever read in a book about theory before. I’m a bit scared!

About fifteen years ago, I attended a talk by Roger Penrose at the Edinburgh Science Festival on the topic of Gödel’s incompleteness theorem. After Penrose finished delivering the talk, an elderly gentleman in the audience stood up and said that he didn’t really see what the fuss was about. You shouldn’t worry, he asserted, that it’s been shown that every formal system has a ‘tricky’ statement (ie. true but not provable). Chances are, it’s not a very interesting statement. And, besides, if you really cared about it, you could just extend your formal system to assert that it’s true. “Ahh”, said Penrose, “but now that new system you’ve created will have it’s own unprovable statement!”. The elderly gentlement was not impressed. “Well then”, he said, “I’d just add a new rule to that one too!”. Penrose noted that the augmented system would suffer the same incompleteness fate, but the elderly gentleman was prepare to keep adding more rules for as long as it took, and the session briefly descended into farce.

At the time, I thought the guy was missing the point. After all, it’s the incompleteness of any given formal system which matters – patching the formal systems with duct tape moves the goal posts but doesn’t let you escape the problem.

But, with a more engineering mindset on today, what he said seems quite reasonable. Most of the time, the incompleteness or undecidability of a formal system doesn’t stop you doing lots of interesting things with it. I don’t worry about the halting problem when I start up firefox, and my high school maths teacher seemed unconcerned that my homework submissions might contain a true-but-unprovable statement. I’m also reminded of a quote I read a long time ago in a paper about the dependently-typed language, Cayenne:

“So type checking Cayenne is undecidable. This is unfortunate, but unavoidable for a language like Cayenne. How bad is it in practice to have an undecidable type checker? This question can only be answered by practical experiments. The Cayenne programs we have tried to date range from ordinary Haskell style programs, to programs using dependent types, to proofs of mathematical propositions. The total size of these programs are only a few thousand lines, but so far the experience shows that it works remarkably well.

Having undecidable type checking means that the type checker might loop. This is clearly not a user friendly type checker. So instead the implemented type checker has an upper bound on the number of reduction steps that it may perform. If this limit is exceeded the type checker will report this. Most of the type errors from the Cayenne compiler are similar to those that any other language would give. Very infrequently does the type checker report that it did not terminate within the prescribed number of steps. Most often, this is the result of a type error, but sometimes the type expression is just too complicated and the number of reduction steps must be increased (the number of reduction
steps is a compiler arg).”

Anyhow, to come full circle, the reason that I remember all this tonight is that I just found out that Alan Turing’s thesis was on exactly the topic which the elderly gentleman was riffing on. In essence, what happens when you keep patching your formal system, Wily Coyote stylee, to build an ACME infinite series of formal systems, each a litle bit better that the one before? I have not read the thesis yet, but I found it amusing to note that, with hindsight, the eldery gentleman from fifteen years ago was onto something!