Der Linux Stiftungdas gemeinnützige Technologiekonsortium, das verschiedene Open-Source-Bemühungen verwaltet, gab heute die Markteinführung des TLA+ bekannt Stiftung Förderung der Einführung und Entwicklung der Programmiersprache TLA+. AWS, Oracle und Microsoft gehören zu den Gründungsmitgliedern.
Was ist die Programmiersprache TLA+, fragen Sie? Es ist eine formale „Spezifikationssprache“, die von dem Informatiker und Mathematiker Leslie Lamport entwickelt wurde. Lamport – heute Wissenschaftler bei Microsoft Research – ist vor allem für seine wegweisende Arbeit im Bereich verteilter Systeme bekannt und hat TLA+ entwickelt, um Softwareprogramme zu entwerfen, zu modellieren, zu dokumentieren und zu verifizieren – insbesondere solche der gleichzeitigen und verteilten Variante.
Um nur einige Beispiele zu nennen: ElasticSearch, die Organisation hinter der gleichnamigen Suchmaschine, verwendete TLA+, um die Korrektheit ihrer verteilten Systemalgorithmen zu überprüfen. An anderer Stelle verwendete Thales, der Hersteller elektrischer Systeme, TLA+, um fehlertolerante Module für seine industrielle Steuerungsplattform zu modellieren und zu entwickeln.
„TLA+ ist insofern einzigartig, als es für die Spezifizierung eines Systems und nicht für die Implementierung von Software gedacht ist“, sagte ein Sprecher der Linux Foundation per E-Mail gegenüber Tech. „Basierend auf mathematischen Konzepten, insbesondere der Mengenlehre und der temporalen Logik, ermöglicht TLA+ den formalen und rigorosen Ausdruck der gewünschten Korrektheitseigenschaften eines Systems.“
TLA+ enthält einen Modellprüfer und Theorembeweiser, um zu überprüfen, ob die Spezifikation eines Systems die gewünschten Eigenschaften erfüllt. Das Ziel besteht darin, Entwicklern dabei zu helfen, über Systeme oberhalb der Codeebene nachzudenken und (hoffentlich) Designfehler aufzudecken und zu verhindern, bevor sie sich in den späteren Phasen der Softwareentwicklung zu Fehlern entwickeln.
Bis zu diesem letzten Punkt sind Fehler im Softwaredesign überraschend häufig – und störend. Ein 2020 Bericht von der Standish Group fanden heraus, dass rund 66 % der Softwareprojekte scheitern. Und nach Laut dem Consortium for Information and Software Quality kostet schlechte Softwarequalität Unternehmen im Jahr 2020 über 2 Billionen US-Dollar.
Mit der Gründung der TLA+ Foundation sagt die Linux Foundation, dass sie Bildungs- und Trainingsressourcen rund um TLA+ bereitstellen, Forschung finanzieren und Tools dafür entwickeln und daran arbeiten wird, eine Gemeinschaft von TLA+-Praktizierenden zu fördern. Die TLA+ Foundation wird auch Entscheidungen über Sprachverbesserungen treffen, auf Benutzerfeedback eingehen und die Entwicklung der Sprache leiten.
„TLA+ wurde bereits erfolgreich von großen Technologieunternehmen wie Amazon, Oracle und Microsoft eingesetzt, um Systeme im planetaren Maßstab zu verifizieren und zu entwerfen“, fuhr der Sprecher fort. „Durch die Gründung einer TLA+ Foundation unter dem Dach der Linux Foundation wird TLA+ an Sichtbarkeit und Unterstützung gewinnen und seine breitere Akzeptanz in der Technologiebranche fördern. Die Mission der Stiftung, sich für Open-Source-Projekte einzusetzen, wird sicherstellen, dass sich TLA+ weiterentwickelt und für die breitere Tech-Community zugänglich bleibt. Darüber hinaus wird die Stiftung eine stärkere Zusammenarbeit zwischen Industrie und Wissenschaft erleichtern und den Stand der Technik in Bezug auf formale Methoden sowie die Forschung zu gleichzeitigen und verteilten Systemen vorantreiben.“