インタビュー
ガブリエラ・モレイラ、Quint at Informal SystemsのCEO – インタビュー・シリーズ
ガブリエラ・モレイラ、Quint at Informal SystemsのCEOは、プログラミング言語と形式手法を専門とする研究エンジニアで、複雑なシステムの検証をエンジニアによりアクセスしやすくするツールを構築することに強い焦点を当てています。她は、TLA+に基づくモダンな実行可能な仕様言語であるQuintの開発を主導し、言語とツールを維持および進化させ続けています。彼女の仕事は、形式検証、静的解析、開発者ツールにわたるもので、形式手法を教えることで学術界にも貢献しており、実践的なエンジニアリングと理論的深さの融合を示しています。
Quintは、Informal Systemsで開発および維持されているモダンな仕様言語で、分散ネットワーク、ブロックチェーン、データベースなどの複雑なシステムをモデル化、テスト、検証するように設計されています。TLA（時相論理アクション）の基盤に築かれたQuintは、開発者に優しい構文を導入し、型チェック、シミュレーション、モデルチェックなどの高度なツールを提供し、エンジニアがデプロイ前にシステムの故障を検出できるようにします。プラットフォームは、実行可能な仕様を重視し、開発者がシステムの動作を記述するだけでなく、実際にテストして探索できるようにします。理論的な正しさと実世界の実装の間のギャップを埋めます。
最初から戻って、プログラミングに興味を持つきっかけは何でしたか？また、形式手法や分散システムに取り組むようになった経緯は何ですか？
私はゲーム好きで、悪いコンピュータを持っていました。私は問題を解決し、動くようにすることが好きでした。私はコンピューターサイエンスに登録し、理論とコンパイラに惹かれました。
2015年、私はプログラミングコンテストに出会いました。そこでは、入力と期待される出力の例が数個与えられ、問題を解決するコードを書きます。しかし、評価のために提出すると、コードは実際には多くの例でテストされます。コードが私の想像したシナリオで動作するかもしれないが、考慮していないシナリオでは失敗する可能性があるという認識が、プログラミングを私が愛する挑戦に変えました。
業界で働いていると、分散システムに引き寄せられました。そこでは、メッセージが到着する順序、異なる故障モード、多くの隠れた動作を考慮する必要がありました。2018年、同僚が私にTLA+という形式仕様言語を紹介しました。私はすぐにその魅力に惹かれました。私はTLA+の周りのツールを構築し始め、以来この分野で働いてきました。
あなたは形式手法とプログラミング言語を中心にキャリアを築いてきました。TLA+に基づくツールの初期の作業から、Informal SystemsでのQuintの開発を主導するまで。形式検証をよりアクセスしやすくすることに焦点を当てるきっかけは何でしたか？また、そのビジョンはQuintの設計にどのように影響しましたか？
TLA+は、業界で広く使用されるに値するものです。私はまだ若かったときにTLA+を学び、同僚と一緒に解決策を検討するために電話に参加していました。私は常に、シナリオで私たちの解決策が失敗するのを防ぐ最後の防衛線でした。しかし、常にそのシナリオに対して最後の防衛線になることは、コストがかかりすぎることになります。したがって、コードを実装する前に仕様を作成するための形式手法の使用というアイデアが生まれました。私はその道に進み、Informal SystemsとQuintにたどり着きました。
Quintは最初、製品として考えられていませんでした。私たちは、Informal Systemsで必要なシステムの信頼性を高めるためにTLA+の仕様を書いていました。しかし、TLA+の構文が怖く、多くの数学的な記号があり、ツールが人の基本的な期待を満たしていませんでした。私たちは同僚や外部の協力者に「見てください、私がやってみたこと」という感じで見せましたが、彼らは読むことができず、ツールを学ぶ時間がありませんでした。
Quintの設計選択は、その経験から直接生まれました。言語は読みやすく覚えやすいです。私たちが最初に構築したのは、VSCode拡張機能でエラーを強調表示するものでした。型と明確なモードがあり、層を明確に分離します。REPLがあり、対話的に探索できます。シミュレーターがあり、迅速なフィードバックを得て反復することができます。標準化されたJSON形式でトレースをエクスポートし、機械が解析しやすい形式です。これらは、プログラマーが既にツールから期待しているもので、私たち自身も必要なものでした。下層の検証は、TLA+と同じ論理です。
私は形式手法をよりアクセスしやすくすることに情熱を傾けています。ツールを出荷することは興奮しますが、実際の影響は、エンジニアリングチームが実際にそれらを使用する場合にのみ感じられます。ツールができることと、開発者にとって有用に感じることの間にはまだギャップがあります。そのギャップを埋めるために努力しています。
Quintについて読者が不明な場合は、Quintは何ですか？また、既存のツール seperti TLA+と比較して、新しい仕様言語が必要な理由は何ですか？
ほとんどの仕様は、ドキュメントです。システムが何をするべきかを記述し、読み取りによってそれを確認します。問題は、ドキュメントが機械的に検出できない方法で間違っていることです。名前が定義されていない、動作が曖昧である、暗黙の仮定があるなどです。通常、実装中に、または本稼働中にそれを発見します。
Quintの仕様は、実行可能なものです。システムを状態マシンとしてモデル化し、満たすべき特性を定義し、モデルを実行または検証します。違反がある場合、正確なシーケンスのステップを示す反例が得られます。那は、設計上の欠陥を検出するときと、どのくらい安価に検出できるかを変えます。
TLA+はこれを常にできました。Quintは、時相論理の専門家でないエンジニアにとって実用的です。
Quintは、形式手法と日常のソフトウェアエンジニアリングの間のギャップを埋めるように設計されています。従来のアプローチと比較して、どのような使いやすさの障壁を排除しようとしましたか？
正直に言えば、最大の使いやすさの障壁は構文でした。那が、私たちが最初に取り組んだことです。構文を解決した後、他の要因に焦点を当てることができました。Quintの型と効果システムは、検証プロセスを開始する前にできるだけ多くのエラーをフラグにするために導入されました。人々はそれを大いに評価しました。那により、高品質な仕様がより多くの人々によって読めるようになりました。私たちはそれをエディターに統合し、基本的な機能を提供しました。開発者が期待する権利です。
構文以降で最大の影響を与えたのは、私たちのシミュレーターでした。最初は、システムの動作について最初のフィードバックを提供する方法として導入されました。開発者はコードを書いた後、コードを実行したいとします。それは、検証で処理できるよりも大きな仕様に対する自信を得るための方法として極めて貴重でした。専門家が仕様を検証可能なものに適応させるノウハウは当たり前ではなく、シミュレーターは自信をよりアクセスしやすくしました。私たちはそれを多くのプロジェクトで広く使用しています。
TLA+構文で私の最大の痛みは、バックスラッシュと通常のスラッシュを混同する頻度でした。多くのタイプが必要です。Quintの構文は私の方が好きですが、私が戻ることができないのは、ツールのすべてです。
Quintの1つの強みは、デプロイ前に分散システムをモデル化およびテストできることです。これは、ブロックチェーンやリアルタイムインフラストラクチャのようなシステムを構築する際のエンジニアの考え方をどのように変えますか？
最大のシフトは、検証を早めることです。TLA+の創設者であるレスリー・ランポートは、コードを書く前に仕様を書くことを、建設作業前に青写真を描くことと比較しています。何かをすでに構築した場合でも、現在青写真を書き、変更を通知することは良い考えです。
ソフトウェア業界では、Markdownファイルとホワイトボードを使用します。テキストで建物を説明しようとすることと比較できます。機能しますが、壁のサイズが合計するかどうかを知ることができますか？Quintは、システムを記述できる方法を提供し、高レベルで記述できます。動作と正しさについての洞察を得ることができます。
QuintはTLA+の基盤に築かれています。理論的な厳格さを維持しながら、言語をより開発者に優しいものにする方法は何でしたか？
鍵となる決定は、QuintをTLA（TLA+の背後にある論理）の断片に制限することでした。TLAは非常に表現力がありますが、その表現力の中には、ツールによってサポートされていない演算子や、人々が理解して使用するが、デバッグが非常に難しい組み合わせが含まれます。私たちは、現実的な仕様が実際に必要とするものに従い、混乱の可能性を避けることを選択しました。
型システムと効果システムは、有用な制約を追加します。Specエラーの全クラスを防ぎますが、それらは検証が実行されている後に発見されるのが楽しくないものです。型はほぼ完全に推論され、効果はユーザーから隠されています。価値を追加するのに、摩擦はありません。
私がTLA+の存在を知る前に、私は型システムの研究を行っていました。Quintの型チェッカーを書くのが、私の好きなコンポーネントでした。私は、Paçoca風味のコーヒーを飲みながら、初期の数ヶ月間で型システムの論文をレビューし、「私の生活は素晴らしい」と考えました。
言語を使用しやすくしながら、TLA+との対応を維持する（Quintの仕様はTLA+に変換できる）ことは、プログラミング言語の演習でした。チームとの議論は、最も役立つリソースでした。初期のユーザーのフィードバックに続きます。まだ改善したい点がありますが、それが私の仕事で最も好きな部分かもしれません。
あなたは静的解析や型システムにも取り組んでいます。これらの経験は、Quintの型チェック、ツール、全体的な開発者体験にどのように影響していますか？
私がその世界で学んだ最大の教訓は、すべての言語が同じではないということです。人々は、単に新しい構文を学ぶことだけが必要で、同じ概念が適用されるため、すべての言語は等しく、単に好みの問題であると言います。那は真実ではありません。プログラミング言語の分野には、素晴らしい研究者がこの分野を進歩させるために働いています。那は、言語をより美しく見せるか、より好みに合うようにするためだけではありません。
関数型プログラミングは私に初めから紹介されました。私はHaskellを同時に学びました（私の最初のプログラミング言語はCでした）。私はそれに非常に感謝しています。那は、私がQuintで状態の変化と非決定性を薄い層に分離し、すべての複雑さを純粋な関数に持たせるのに役立つ基盤です。那は、好みの問題だけではありません。好みの問題が頻繁に議論される場合、Quintを構築することは生産的ではなかったでしょう。
形式手法を講師として教えることは、あなたに独自の視点を与えています。エンジニアが現在形式検証について持っている最も一般的な誤解は何ですか？
私は、業界で初めて働くことを目指していた大学生を教えていました。ほとんどの学生は、形式手法や形式検証について以前聞いたことがありませんでした。誤解はありませんでした。カリキュラムは、ほとんどの学生が形式手法や分散システムについて学ばないように設計されていました。半分の学生は、同じ学期にスレッドについて学びました。私は、雨を経験する前に、どのように傘の使い方を教えるようなものだと感じました。
私は、形式手法と形式的にシステムを仕様化することで、解決策について推論し、エッジケースを見つけるのに役立つことを教えることに重点を置きました。すべてのソフトウェアに形式検証を使用する必要があると考えるのではなく、将来仕事で同様の状況に直面したときに私を思い出してくれることを希望しました。何人かはすでにそうしています。
AIとソフトウェア開発の組み合わせへの関心が高まっています。Quintのようなツールを使用して形式的な仕様を書く、検証する、または生成するのを支援するために、開発者にとってAIの役割を見ていますか？
大きい役割があります。すでに起こっています。コンピューターサイエンスは、コードを書くことよりも広い分野です。AIは、形式手法を使用するための新しい方法を開拓しています。LLMは、自然言語のシステムの説明からQuintの仕様を書くことができ、さらには既存のコードからです。Quint LLMキットには、英語の説明からQuintの仕様を生成するClaude Codeエージェントが含まれています。
同時に、Quintは、AIで書かれたコードを信頼するのを支援します。私は、信頼は、魔法のようなチェックマークではなく、理解から来るべきだと強く信じています。Quintの仕様を書き、実装コードを駆動およびチェックすることで、開発者はシステムの動作を所有および理解できます。AIの使用によって生じる認知的負債に対処し、生成されたコードを検証するためのより断定的方法を提供します。
私たちは、自然言語の意図からQuintの正確な定義を書く言語ツールとしてLLMを活用し、QuintのツールをAIに提供して、AI単独では信頼性が低いエッジケースを見つけるなどのタスクを実行できるようにします。
形式手法がニッチな採用から、ソフトウェア開発ライフサイクルの標準的な部分になるために何が必要ですか？
しばらくの間、私がQuintに必要な2つの高レベルのことは、コストの低減と価値の向上です。私は、これが他の多くのことにも当てはまるのではないかと思います。形式手法は、AIによってコストと価値の両方で大きなブーストを得ました。AIは、形式的な仕様を書くコストを大幅に削減し、また、信頼と理解の欠如の環境を作り出すことで、形式手法が最も影響力があり価値のあるものになるのを助けています。
AIが私たちの職業を変えている間、私は、変化がより高レベルの設計選択と動作の正しさに向かっていることを希望します。形式手法が日常のツールになることです。私たちがコードやシステムを理解しないまま、AI生成のコードをレビューするのに時間を費やすのではなく、形式手法が毎日のツールになることを希望します。
感謝の意を表します。このインタビューは、Quintについてさらに学びたい読者にとって、実行可能な仕様言語であるQuint、ツール、開始方法についての詳細を提供しています。Quint。
