Rekursive Lösung in JavaScript

[1unitedpower]

Die Aufgabenstellung hat mich übrigens an meine Vorlesungen „Einführung in die Programmierung“ und „Paradigmen der Programmierung“ erinnert.

Die Übungsblätter dazu habe ich echt genossen; eine Lösung zu programmiertechnischen Problemen zu finden ist eine Aufgabe mit sehr selbstbelohnendem Charakter.

So viel Genugtuung wie ein gelöstes Programmierproblem hat mir ein selbst geglückter Beweis eines mathematischen Satzes noch nie bereitet.

Am schönsten ist es, wenn man beides kombiniert, sagt dir der Curry-Howard isomorphism etwas? Intuitiv sagt der aus, dass Programme in rein funktionalen Sprachen, das gleiche sind wie Beweise. Der Typ eines Ausdrucks kodiert einen Satz oder eine Proposition, die Implementierung ist der Beweis dafür, dass der Satz bzw. die Proposition unter gewissen Umständen hält. Um damit auch Beweise über nicht-triviale Eigenschaften machen zu können, muss das Typsystem der Programmiersprache allerdings auch über eine entsprechende Aussagekraft verfügen. Das trifft derzeit leider nicht mal auf Haskell zu, obwohl es sich dahin bewegt. Idris ist eine Programmiersprache, die extra für Programmier entworfen wurde um dieses Paradigma voranzutreiben. Für Mathematiker existieren schon länger vergleichbare "Programmiersprachen", z.B.Coq und Isabelle.