ガブリエラ・モレイラ、QuintのCEO at Informal Systems – インタビュー・シリーズ

ガブリエラ・モレイラ、QuintのCEO at Informal Systemsは、プログラミング言語と形式手法を専門とする研究エンジニアで、複雑なシステムの検証をエンジニアにとってよりアクセスしやすくするツールを構築することに重点を置いています。彼女は、TLA+に基づく現代的な実行可能な仕様言語であるQuintの開発を主導し、言語とツールを維持および進化させています。彼女の仕事は、形式検証、静的解析、開発者ツールにわたるもので、形式手法を教えることで学術界にも貢献しており、実践的なエンジニアリングと理論的な深さの融合を示しています。

Quintは、Informal Systemsで開発および維持されている、分散ネットワーク、ブロックチェーン、データベースなどの複雑なシステムをモデル化、テスト、検証するための現代的な仕様言語です。Temporal Logic of Actions (TLA+)の基盤に構築されたQuintは、開発者に親しみやすい構文と、型チェック、シミュレーション、モデルチェックなどの高度なツールを導入し、エンジニアがデプロイ前にシステムの障害を検出できるようにします。プラットフォームは、実行可能な仕様を重視し、開発者がシステムの動作を記述するだけでなく、実際にテストして探索できるようにします。これにより、理論的な正しさと実世界の実装の間のギャップを埋めます。

最初から戻って、プログラミングに興味を持つきっかけは何でしたか？そして、形式手法と分散システムに取り組むようになったのはどうなりましたか？

私はゲームが好きで、悪いコンピューターを持っていました。問題を修正し、動作させることができたので、コンピューター・サイエンスに興味を持つようになりました。理論とコンパイラに惹かれました。

2015年、私はプログラミング・コンテストに出会いました。コンテストでは、入力と期待される出力の例が与えられ、問題を解決するコードを書きます。しかし、評価のために提出すると、コードは多くの例でテストされます。コードが見えているシナリオや、私が考えるシナリオで動作するかもしれませんが、考慮していないシナリオでは失敗する可能性があるという認識が、プログラミングを挑戦に変えました。

業界で働いていると、分散システムに惹かれました。メッセージが到着する順序、異なる障害モード、多くの隠れた動作を考慮する必要があります。2018年、同僚が私にTLA+という形式仕様言語を紹介しました。私はすぐにそれに夢中になりました。TLA+の周りのツールを構築し始め、それ以来この分野で働いてきました。

あなたは形式手法とプログラミング言語を中心にキャリアを築いてきました。Quintの開発を主導するに至った動機は何でしたか？そのビジョンはQuintの設計にどのように影響しましたか？

TLA+はあまりにも優れているので、業界で広く使用されるべきです。私はまだ若かったときにTLA+を学び、同僚と一緒に解決策を探すために電話会議に参加していました。私は常に最後の防衛線でしたが、シナリオで解決策が失敗することがありました。もっと良い方法があるはずです。形式手法を使ってコードを実装する前に仕様を作成するというアイデアが生まれました。そこで、私は学術的な旅を始め、Informal SystemsとQuintにたどり着きました。

Quintは最初、製品として考えられていませんでした。私たちは必要性からそれを作りました。私たちは、より信頼できるシステムのTLA+仕様を書いていましたが、構文が怖く、ツールが基本的な期待を満たしていませんでした。同僚や外部のコラボレーターに「見てください、私がやった素晴らしいこと」と言ったのですが、彼らは読むことができず、学ぶ時間がありませんでした。

Quintの設計はその経験から直接生まれました。言語は読みやすく覚えやすいです。最初に作ったのは、エラーを強調表示するVSCode拡張機能でした。型と明示的なモードがあり、REPLとシミュレーターがあり、迅速なフィードバックを得ることができます。標準化されたJSON形式でトレースをエクスポートします。これらは、プログラマーがすでに期待しているツールでした。形式手法の下にある検証はTLA+と同じです。

Quintは、分散システムをデプロイ前にモデル化およびテストする能力を持っています。エンジニアがブロックチェーンやリアルタイム・インフラストラクチャーのようなシステムを構築するときに、考え方を変える必要がありますか？

最大の変化は、検証を早めることです。Leslie Lamport、TLA+の作者は、コードを書く前に仕様を書くことを、建設作業前に青写真を書くことと比較しています。すでに何かを構築した場合でも、現在の変更を通知するために仕様を書くことは良い考えです。

ソフトウェア業界では、マークダウンファイルとホワイトボードを使用します。建物をテキストで説明することと比較できます。機能しますが、壁のサイズが合計するかどうかはわかりません。Quintは、システムを説明する方法を提供し、高レベルでインサイトを得ることができます。

QuintはTLA+の基盤に構築されています。理論的な厳格さを維持しながら言語をより開発者に親しみやすくするには、どうバランスをとることができましたか？

重要な決定は、QuintをTLAの断片に制限することではなく、TLAが許可するすべてを公開することではありませんでした。TLAは非常に表現力がありますが、その表現力の一部には、ツールによってサポートされていない演算子や、人々が間違って使用し、デバッグが非常に難しい組み合わせが含まれます。私たちは、実用的ではない選択をしました。ほとんどの現実的な仕様が実際に必要とするものに従い、混乱の可能性を避けます。

あなたは静的解析と型システムも取り組んでいます。Quintの型チェック、ツール、開発者体験にどのように影響していますか？

プログラミング言語の分野には、素晴らしい研究者がこの分野を進歩させるために働いています。機能プログラミングは私に早くから紹介されました。Haskellを同時に学びました。Quintでは、状態の変化と非決定性を薄い層に分離し、すべての複雑さを純粋な関数に置くことが、多くの要因で役立つことを示しています。Quintを構築することは、たまたま好みの問題でなければ、生産的ではなかったでしょう。

形式手法を講師として教えることで、エンジニアが形式検証について持っている最も一般的な誤解は何ですか？

私は、業界で初めての学生たちに教えていました。ほとんどの学生は、形式手法や形式検証について以前聞いたことがありませんでした。私は、形式手法や形式仕様が解決策やエッジケースを理解するのにどのように役立つかを教えることに重点を置きました。彼らに、すべてのソフトウェアを形式的に検証する必要はないと伝えました。私の最終的な課題は、テーブルトップRPGの設定で、プレイヤーが取る順序や設定を考慮する必要があり、分散システムの難しさをできるだけ模倣することでした。彼らはツールを使用してエッジケースを見つけて解決を改善する必要がありました。彼らは私を覚えていることを願います。すでに何人かはそうしています。

ソフトウェア開発にAIを組み合わせることに興味が高まっています。Quintのようなツールを使用して、開発者が形式的な仕様を書き、検証、または生成するのを支援する役割がありますか？

大きな役割があります。コンピューター・サイエンスはコードを書くことよりも広い分野です。AIは、形式手法を使用する新しい方法を開拓しています。LLMは、自然言語のシステムの説明からQuintの仕様を書くことができ、既存のコードからも仕様を生成できます。Quint LLMキットには、プロトコルの英語の説明からQuintの仕様を生成するClaude Codeエージェントがあります。

同時に、Quintは、AIによって書かれたコードを信頼するのを支援します。私は、信頼は理解から来るべきだと強く信じています。Quintの仕様は、実装コードを駆り立て、チェックするものです。開発者はシステムの動作を理解し、AIの使用によって生じる認知的負債を解決し、生成されたコードを検証するためのより断定的方法を提供します。

形式手法がニッチな採用から、ソフトウェア開発ライフサイクルの標準的な部分になるために何が必要ですか？

しばらくの間、私はQuintがより広く採用されるために必要な2つの高レベルのものを知っていました。コストを下げ、価値を高めることです。これは、他の多くのことにも当てはまります。形式手法は、AIによって大きなブーストを受けました。AIは、形式的な仕様を書くコストを大幅に削減し、形式手法が最も影響力があり、価値がある環境を作り出しています。

AIが私たちの職業を変えているので、私はこの変化が、高レベルの設計選択と動作の正しさに向かっていることを願っています。形式手法が日常のツールになることを願っています。私たちは、コードやシステムを理解することができず、AIによって生成されたコードを検証するためのツールセットなしで、すべての時間を費やすことになるのではないことを願っています。

感謝を込めて、このインタビューで、複雑なシステムをモデル化および検証するための実行可能な仕様言語、ツール、開始方法についてさらに学びたい読者向けに、Quintを探索できます。