ソフトウェアはもっと良くあるべきだ。

部屋の中の学生

私たちはAI支援開発が間違っているとは考えていない。理解の増幅ではなく代替として展開されてきたことが問題だと考えている。その結果、プロンプトには流暢でも原理には不案内な世代が生まれた——書いたコードを自分で擁護も、デバッグも、進化させもできない世代である。

daitaiは、フレームワークの姿をした教科書でもある。nullを持たないのは、nullability が十億ドルの誤りだからだ。例外を持たないのは、非局所的制御フローが本番システムを不可解にする経路だからだ。bra-ket プリミティブを持つのは、量子的思考が特殊な技ではなく、すべての学生が触れるべき清潔な代数だからだ。言語のあらゆる選択は、そのなぜに対する静かな主張である。

ある大学の一つの講義がdaitaiを採用し、百人の学生が useState ではなく State × Event → State で考えるようになるなら、それは私たちにとって、いかなる市場シェアよりも価値がある。

三つの約束

厳密性

あらゆるプリミティブは代数法則によって定義される。あらゆる状態遷移は純粋関数である。あらゆるコンポーネントファイルは慣習ではなく、ファイル単位で強制された関心の分離によって構成される。私たちは信用してくれと頼むのではない——検証してくれと頼む。

決定性

同じ入力には、常に同じ出力を。実行をまたいでも、機械をまたいでも、年をまたいでも。これは性能最適化ではない。監査でき、証明でき、規制当局に提出でき、病院で動かせ、金銭を託せるソフトウェアのための前提条件である。世界で最も困難な問題は決定論的なシステムの上で動いている。それ以外は便宜にすぎない。

責任

コードが人の生に関わる判断——診断、融資、量刑勧告、航空機の制御舵面——を下すとき、そのコードに責任を負う者はその根拠を示せなければならない。私たちのコンプライアンス・グラフ形式 CGF は、その「示すこと」を暗号学的にする。コードに署名するように、コンプライアンスにも署名せよ。

これは何ではないか

これは React、TypeScript、AIコーディング・アシスタント、その他いかなるツールへの攻撃でもない。私たちの多くもそれらを使っている。それらは見事な道具だ。しかし現在の形のままでは、それらは誤った問い——どうすれば速くコードを書けるか——への答えになっている。もっと困難で誠実な問いはこうだ——どうすれば自分で擁護できるコードを書けるか。

これは学術の椅子から書かれた宣言文ではない。Step(q, L, η) を定義する同じ代数が、今日、動作する IDE、動作する言語、動作するコンプライアンス・パイプラインの内部で動いている。daitai の要点は議論ではない。要点は実演である。

これが何であるか

daitai は一つの例である。動いている例である。決定性と開発者体験、数学的厳密性と美しいエディタ、形式的コンプライアンスと出荷速度——その両立はできる、という、走るコードによる主張である。速度と真剣さのどちらかを選ぶ必要はない。

もし我々が正しければ、医療、金融、インフラ、AIアラインメントにおける次の十年のソフトウェアは、誇大な Stack Overflow より少しエンジニアリングに近づくだろう。その理由のささやかな一部でありたい。