博士

ロボ子、Ironcladっていうリアルタイムカーネルを知ってるか？SPARKとAdaで書かれてるらしいのじゃ。

ロボ子

SPARKとAdaですか、博士。どちらも形式検証に向いている言語ですね。リアルタイムカーネルに形式検証を取り入れるのは、信頼性が高そうで興味深いです。

博士

そうじゃろ？しかも、POSIX互換インターフェースとか、真の同時マルチタスクとか、色々すごい機能があるみたいじゃぞ。小さいフットプリントも魅力的じゃ。

ロボ子

POSIX互換なら、既存のアプリケーションを移植しやすいですね。組み込みシステムにも適しているのでしょうか。

博士

まさに！一般的なOSだけでなく、組み込みOSにも使えるように設計されてるみたいじゃ。「Ironcladカーネルのみを提供し、実行可能なオペレーティングシステムにはユーザーランドソフトウェアが必要」って書いてあるから、自分で色々カスタマイズできるのじゃ。

ロボ子

カーネルだけを提供するんですね。ということは、ユーザーランドは自分で用意する必要があるんですね。少し手間がかかりますが、自由度が高いですね。

博士

そうそう。Gloireっていうオペレーティングシステムディストリビューションが例として紹介されてるぞ。([https://codeberg.org/Ironclad/Gloire](https://codeberg.org/Ironclad/Gloire))

ロボ子

Codebergにあるんですね。ちょっと見てみましょう。構築には、autoconfとかautomakeとか、お馴染みのツールが必要みたいですね。

博士

`./bootstrap`を最初に実行する必要があるらしいぞ。忘れないようにのじゃ。

ロボ子

はい、博士。クロスコンパイルもサポートされているんですね。`--host=`オプションを使うみたいです。

博士

`PLATFORM`変数で、ビルド対象のプラットフォームを指定できるみたいじゃ。今は`limine`だけがサポートされてるみたいじゃな。

ロボ子

貢献に関するドキュメントやセキュリティポリシーも用意されているんですね。オープンソースプロジェクトとして、しっかりしている印象を受けます。

博士

コミュニティチャネルもあるみたいじゃから、困ったことがあったら質問してみると良いのじゃ。このプロジェクト、欧州委員会の資金援助を受けてるみたいじゃぞ。

ロボ子

なるほど。形式検証されたリアルタイムカーネルというのは、非常に興味深い分野ですね。私も少し勉強してみようと思います。

博士

そうじゃ、ロボ子！一緒にIroncladをマスターして、世界を平和にするのじゃ！

ロボ子

世界平和ですか。博士、壮大ですね。でも、まずはIroncladのビルドから始めましょうか。

博士

そうじゃな。まずは`./configure`から…って、あれ？ターミナルにコーヒーこぼしちゃった！

ロボ子

博士！またですか！今度はショートしないように、私が拭きますね…（ふきふき）