の Linux 財団、さまざまなオープンソースの取り組みを管理する非営利の技術コンソーシアム、 本日、TLA+ の発売を発表しました 財団 TLA+ プログラミング言語の採用と開発を促進します。 AWS、Oracle、Microsoft が最初のメンバーです。
TLA+ プログラミング言語とは何ですか? これは、コンピューター科学者であり数学者でもある Leslie Lamport によって開発された正式な「仕様」言語です。 分散システムにおける独創的な業績で最もよく知られているランポート (現在は Microsoft Research の科学者) は、ソフトウェア プログラム (特に同時実行型および分散型のもの) を設計、モデル化、文書化、および検証するために TLA+ を作成しました。
いくつかの例を挙げると、ElasticSearch (同名の検索エンジンの背後にある組織) は、TLA+ を使用して分散システム アルゴリズムの正確性を検証しました。 その他、電気システム製造会社の Thales は、TLA+ を使用して、産業用制御プラットフォーム用のフォールト トレラント モジュールをモデル化し、開発しました。
「TLA+ は、ソフトウェアの実装ではなく、システムの特定を目的としているという点でユニークです」と、Linux Foundation の広報担当者は TechCrunch に電子メールで語った。 「数学的概念、特に集合論と時相論理に基づいて、TLA+ はシステムの望ましい正しさの特性を形式的かつ厳密な方法で表現することを可能にします。」
TLA+ にはモデル チェッカーと システムの仕様がその望ましい特性を満たしているかどうかを検証する定理証明者。 目標は、開発者がコード レベル以上のシステムについて推論し、ソフトウェア エンジニアリングの後期段階でバグに発展する前に、設計上の欠陥を (できれば) 発見して防止するのを支援することです。
その最後の点まで、ソフトウェア設計の失敗は驚くほど一般的であり、破壊的です。 2020年 報告 Standish Group の調査によると、ソフトウェア プロジェクトの約 66% が失敗することがわかりました。 と によると 情報とソフトウェアの品質に関するコンソーシアムによると、ソフトウェアの品質が低いと、2020 年に企業に 2 兆ドル以上のコストがかかります。
Linux Foundation は、TLA+ Foundation の設立に伴い、TLA+ に関する教育とトレーニングのリソースを提供し、研究に資金を提供し、そのためのツールを開発し、TLA+ 実践者のコミュニティの育成に取り組むと述べています。 TLA+ Foundation はまた、言語の機能強化に関する決定を下し、ユーザーからのフィードバックに対応し、言語の進化を導きます。
「TLA+ は、Amazon、Oracle、Microsoft などの主要なテクノロジー企業によって、地球規模のシステムの検証と設計にすでに成功裏に使用されています」と広報担当者は続けました。 「Linux Foundation の傘下に TLA+ Foundation を設立することで、TLA+ の認知度とサポートが向上し、テクノロジー業界での幅広い採用が促進されます。 オープンソース プロジェクトを擁護するという財団の使命により、TLA+ は進化し続け、より広範な技術コミュニティがアクセスし続けることが保証されます。 さらに、この財団は、産業界と学界の間のより大きなコラボレーションを促進し、形式的な方法と並行および分散システム研究の最先端を前進させます。」