IOHKブログ：Cardano構築における形式手法とアジャイル手法の統合
IOHK形式手法ディレクターPhilipp Kantがフレキシビリティと高精度を備えたソフトウェア構築の方法論を紹介
2020年4月9日 Philipp Kant 読了時間7分
形式と関数
IOHKはCardanoをグローバルな金融およびソーシャルオペレーティングシステムへと成長させている。この巨大なタスクは迅速なイテレーションおよび厳密な正確さを必要とする。このためIOHKはアジャイル手法のスピードに保証性の高いコードと形式手法を組み合わせることを選択した。フレキシビリティと形式の融合により、IOHKのエンジニアはこのモダンな開発哲学のパイオニアとなる。
IOHKは研究、形式手法、関数型プログラミング、そして厳密性を持って望む構築スタイルに絶対の信を置いている。ブロックチェーン開発業界における競合者として、我々はまた恒常的に進捗状況を開示し、そのグローバルなステークホルダーによるコミュニティのために価値を生み出さなければならない。これはすなわち、ロバスト性や開発スピードおよびフレキシビリティに妥協が許されないことを意味している。変化し続ける市場においてこれは難しい課題であり、開発者たちにはうまく両立させていくことが要求される。
アジャイル性対形式性
技術開発を開始する際の標準は最小規模製品（MVP）を素早く構築し、マスマーケットに適したものとなるまでイテレーションを繰り返すというものだ。これはアジャイルプロセスとして知られる、完全に機能する製品を構築するに至るまでの間にプロジェクトの進捗状況を示すのに適した方法だ。しかし、アジャイル手法では開発の各ステップで、後から解決しうるバグや脆弱性があることを想定する。これは価値がリスクに晒されることがなければ問題ないが、暗号通貨の世界では、膨大な金とステークホルダーの信頼がかかっている。
ブロックチェーン上にデジタル資産を構築する場合、開発プロセスを組織するうえで、攻略すべき複数の課題が持ち上がってくる。プルーフオブステークの暗号通貨であるCardanoは、一貫したパフォーマンスが極めて重要となる敵対的環境における分散型システムである。プロトコルは、妨害を試みる悪意のあるアクターに対しセキュリティを維持しなければならない。したがって、素早く構築して問題には後で対処するという余裕はない。
信頼は通貨が受け入れられるうえで不可欠であり、正当性証明はシステムの信憑性を高めるうえで重要な手段である。そのため、コードは正しいだけではなく、広範で有意義なテストや数学的証明のように、その正当性の証拠となるべきものでなくてはならない。暗号通貨のような新興産業において、IOHKエンジニアは、初期バージョンで確立した正当性保証を維持しながら、新機能の追加を予測する必要がある。このプラットフォームは、全ユーザーに対するセキュリティと有効性を維持しながら成長できて初めてスケーリングが可能となる。Cardano開発者が、たとえ要件が変更する中であっても、保証性の高いソフトウェアを作成するために、プロパティベースのテストから機械検証可能証明に至るまで幅広いツールを組み合わせて、その方法論を合理化したのはこのためである。
コード化の研究
方法論は科学的研究から始まる。これまでIOHKは、プラットフォームの作成に貢献する60を超える研究論文を発表している。各論文はブロックチェーン技術の重要な側面を原則から調査している。分散化においてどのようにコンセンサスを得るのか。スマートコントラクトをどのように設計するか。正しい行動をインセンティブ化するために適切な報酬構造とは。IOHKの研究者はこうした設問を調査し、その解答を科学雑誌や学会で発表している。これらの論文には、厳密な査読で認められなければならない証拠が含まれている。次に、ソフトウェアのクオリティに科学が確実に活かされるよう、形式手法を用いて開発を行う。
簡単に言えば、これはIOHKのエンジニアが、コードがすべきことを数学的に特定することを意味する。こうして、コードが実行されるときに意図したとおりの望ましいプロパティが含まれるようにすることができる。コードはHaskellで書かれる。これは強力な型システムを持つ保証性の高い関数プログラミング言語である。Haskellは信頼性のあるソフトウェアの実装に適したツールであるが、フールプルーフではない。したがってコードはテストする必要がある。テストの作成にはQuickCheckの使用が適している。これは、開発者が常にプログラムに保持されているべきプロパティを記述することを可能にする。QuickCheckは次にテストケースを生成し、こうしたプロパティを侵害する最小反例を検索する。
外界とやり取りするコードにおいて、特定のネットワークアプリケーションで、最小反例を見つけるのは困難な場合もある。これは実行の順序に決定性がなく、ソフトウェアが実行されるたびに変更しうるためである。同じコードが何百回と実行でき、失敗するのはたった1回となる。これは、決定性のある実行順序を伴うシミュレーションを使用することで回避できる。シミュレーションでテストを実行することにより、プロダクション環境ではランダムにしか起こり得ないバグの集合を、テストによって確実に発見、修正することができる。
橋を架ける
Cardanoに採用した開発手法は、橋の建設に例えるとわかりやすい。土木技師が橋を建設する際、その時間の多くはデスクで費やされる。土木技師は図面を引き、静的な力を計算し、地質調査を依頼する。この間、建設現場では何も起こらない。観察者はどんな進展も目にすることはできない。橋を建設するなら、これは正しいアプローチだ。プランが正確でなければ、後になって問題を修正するのは難しいしコストもかかる。究極的には、橋の完成は高いコストをかけながら遅れるか、完全な失敗に終わる場合もある。進展が見られないことは、機能的で安全な橋を得るための相応の対価である。
ソフトウェアを構築する際、後になって変更を加えることは建設よりもずっとたやすい。これが一般的なアジャイル手法のアプローチを可能にしている。アジャイル開発者が橋を建設するとしたら、1回の迅速なスプリントで柱を立て、2回目のスプリントで次に進むだろう。橋は最終段階で柱の間に架けられ、うまくいかないことがあればスプリントを追加して修正する。進捗状況は建設現場で明らかにでき、完成した橋には多くの問題が内包されている。このためプロジェクトの最後にはクリーンアップ作業が必要となるが、これは初期段階できちんとプランニングをすることで避けられたことだ。さらに、最小規模製品は一般に少数の人々にテスト目的で配布されるが、これは開発者にバグを警告できるよう失敗を前提としている。言うまでもなく、橋はこの方法でデザインされないのがベストだ。
「形式手法」という言葉を耳にすると、ソフトウェア開発に携わる多くの人々が土木工学のアプローチを思い浮かべる。「ウォーターフォール」と呼ばれ、一般に敬遠される。これは一般的な、不運な誤解である。実際には、適切な形式テクニックを使用すると、ケーキを得るとともにそれを食べることもできる。全体的なデザイン（意図したデザインであり、スプリントで開発したピースを組み合わせることにより偶発的にできるものではない）を得ること、継続的に進捗状況を示すこと、そして、変更が必要な際に反応する能力を維持することである。
IOHK開発者が採用する主要なテクニックとは、実行可能な仕様記述である。これは高レベル設計であり、低レベルのディテールを抽象化し、コンピューターが理解、実行できる言語で書かれる。実行可能な仕様記述は進捗状況を示すためのプロトタイプとして使用し、ユーザーからフィードバックを得、仮定をテストすることができる。さらに、低レベルのディテールを続く改良段階で追加することができる。IOHKの開発者はまず最大の問題を解決するために橋を建設し、後から補強するために柱を追加する。ソフトウェアシステムにおいては、柱はデータをディスクに保存する、あるいは最終製品で必要となるが全体的な機能性を示すうえでは必須ではないパフォーマンスアルゴリズムを使用するといった機能を指す。
実行可能な仕様記述を使用することにより、フレキシビリティを犠牲にすることなく適切なプランニングの利点を得る。IOHK開発者は大きなスケールでシステムがあるべき形に修正し、必要に応じて適切なコンポーネントを実装できる。継続的なテストにより各コンポーネントが全体的なデザインにフィットしていることが保証される。これは後に統合する際に一般に見られる問題の回避に役立つ。この方法論により、両者の長所が得られることになる。トップダウンの設計を使用し（後に統合する際のトラブルを回避し、常時全体的なデザインの手綱を握っていられる）、早期に実用的なコードを得ることができる（進捗状況を示し、全プロセスを通じたテストおよびフィードバックを可能とする）のである。
将来性
究極的に、建設の手法は何を構築するかにより決定されるべきである。IOHKは、厳密さとスピードが求められるグローバルなソーシャルおよび金融オペレーティングシステムを構築している。形式対アジャイルは誤った対立式だ。我々は両アプローチの長所を融合させた独自の方法論を開発し続けている。アジャイルな配信フレームワークにおける形式テクニック。そこには我々の未来すべてを構築することができるロバストで保証性の高いコードがある。