Informal Proof of an Insolvable Problem (with code!)

Chris Wilson is presenting on functional programming in Ruby. See the Tweet that instigated this post here. His slides (possibly revised since this post) got me thinking: how can one describe the Entscheidungsproblem as simply as possible with a programming exercise?

Entscheidungsproblem, the definition of

Entscheidungsproblem is German for "decision problem"; David Hilbert (arguably the most influential German mathematician of the late 19th and early 20th century) posed the problem as a challenge to his formidable colleagues around the world. The goal is to implement an algorithm that tells us whether or not a specific mathematical assertion has a proof. In code, this means code that decides if code evaluates with 100% predictability.

The (Pseudo) Code

/* GoLang */

type FormalLanguage interface{
  Description() rules // describes the language
  Statements() statements // statements of the language
}

func Provable( input FormalLanguage ) output bool {
  // impossible to write algorithm mapping a boolean to each statement
  // of the language
  // the best implementation probably should cause a kernel panic
}

/* Ruby */

module HigherOrderLogic
  def self.provable? statement
    // impossible to write algorithm which returns
    // true iff the statement is provable
    // when correct it should always returns nil!!!
  end
end

The (Informal) Proof

Let's say we had such a function. We would like to implement it where it'd be most useful -- probably as part of an optimization algorithm (in a compiled language), as part of the interpreter (in a dynamic language), or perhaps as a meta-test tool.

Let's put it to work in the testing toolchain. The "provable" function/method could inform the test suite whether the expectation would be met or unmet. One way it might do so would by taking the entire codebase as a description, and a testcase as a statement. The pass/fail outcomes are the obvious ones.

Now, in regular parlance, what does it mean when a testcase returns "true"? Usually, it meets some expectation. What does it mean when an expectation is met? It matches some requirement!

If we wrote code that "knows" how to create expectations from requirements, and also "knows" whether it meets those expectations with some codebase, then both tests and programming would be redundant (or, it would be automated in the sense that the code would update itself according to requirements and derived expectations).

Were we to get to this point, would we implement the Entscheidungsproblem algorithms for our code first, or write the code? If we implement the algorithms, we presume we already know what the code looks like... and our grand goal goes unmet (bonus points: why?) If we write the code, then our implementation of the Entscheidungsproblem is susceptible to the slightest changes in the codebase (bonus points: why?)

Therefore, any implementation of the Entscheidungsproblem will be insufficient.