[linux-l] Verifizierbarkeit bei Rekursion (was: FP/Java vs. OCaml)

[olafBuddenhagen at gmx.net]

Hallo,

> ist der Verzicht auf Rekursion denn Voraussetzung für
> Verifizierbarkeit? Wo hast Du das denn her?

Ich meinte nicht dass Rekursion prinzipiell nicht verifizierbar ist. Es
gibt aber wohl einen bestimmten Subset von ADA, der sich mit heutigen
Mitteln verifizieren lässt, und der soll unter anderem Rekursion
ausnehmen. (Was sonst noch weiß ich nicht.)

Shapiro meinte, damit wäre es zwar möglich, seinen Kernel zu
implementieren, aber nicht zu warten -- dafür ist dieser Subset zu
beschränkt. Deshalb hat er beschlossen die Sache selbst in die Hand zu
nehmen und mit seinen Mannen eine spezielle Sprache zu entwickeln, die
verifizierbar ist, und sich trotzdem zum Schreiben von Mikrokerneln
eignet...

-Olaf-