the soundless interstitium

I received a very fun email from Kartik Agaram in response to my rant on "irresponsible" servers:

I'm reminded of a chapter from Godel, Escher, Bach where Achilles and the Tortoise are arguing some point of logic. From memory, Achilles writes down:

1. A -> B
2. A

Therefore B. But the Tortoise is not persuaded. He says, "where does it say that A and A -> B => B?" So Achilles writes down a new rule:

3. A and (A -> B) -> B

But now the Tortoise refuses to accept the next proposition. And on and on.

It seems valuable to create infrastructure for specifying contracts. But a contract also requires good faith and/or an enforcement mechanism…

semantics

A formal system is unsound if a contradiction can be constructed from a blank slate.

More precisely, a formal system is sound iff all its provable formulas are valid.

When Gödel murdered math, he proved that any formal system that can derive all true statements is guaranteed to be unsound.

And so we know that every sound system has holes.

A sound system is not a sound system.

I call these holes "soundless", since they are neither sound nor unsound.

The fancy term for unprovable/undecidable sentences is "independence", e.g. choice is independent of ZF

applied semantics

Programmers sometimes care about correctness. Good compilers ensure that their programs won't break in obvious ways, i.e. the tree falls in the forest and makes a big sound.

Programming languages offer varying combinations of expressiveness and soundness. Many folks choose languages like Elm for its correctness; many also make equally good arguments for vanilla Javascript's ease/flexibility.

While these languages may be sound, much of the interesting interstitium between clients/servers remains soundless.

Lately, I've been tilting at "irresponsible" servers. If servers could offer guarantees about uptime/protocol, correctness could percolate down to my program at compile time.

Seriously, wouldn't it be nice to deploy a program and be certain that its network dependencies won't break for a few months? Or at least be able to blame a service provider with computational certainty?

Gödel's incompleteness theorems guarantee that soundlessness creeps into sound systems, and that's totally okay; a tattered shirt can still protect you from your nearest star.

Well, this seems rosy and maybe even possible, but who will enforce contracts? Good question! Cryptocurrency is probably dead, but trustless contracts might be salvageable -- or, even better, embrace cheap tech and trust more.

For scrapscript, the architecture is federated, which means you have to trust somebody, but you can choose which somebodies you deem trustworthy. This becomes valuable if, for example, your e-mail provider becomes not not-evil.

I don't know what "enough" soundness sounds like, but REST/gRPC/SOAP/etc. seem subpar. Traffic doubles every 18 months, yet the internet highway experts insist that these paper guardrails are sufficient. Good protocols protect people.

I don't need fancy typeclasses; I don't need smart contracts nor intermediate contract-checkers. I just want my programs to fail loudly as soon as I do something stupid, and especially when that stupidity spans multiple computers.

Anyway, it sometimes seems like trillions of trees are silently falling between every forest. Somebody should probably do something.