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

[Oliver Bandel]

On Wed, Sep 28, 2005 at 12:26:57AM +0200, olafBuddenhagen at gmx.net wrote:
> 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...


interessant.

Haste da mal nen passenden Link?
Gibt's schon nen namen für diese neue Sprache?

Ciao,
   Oliver