ソフトウェア設計は、「誰がどこまで考えるか」を決める仕事である - 変数名からDDD、DB設計、マイクロサービス、組織構造までを同じ枠組みで
ソフトウェア開発には、多くの設計原則があります。 わかりやすい変数名を付ける 関数を小さくする 単一責任にする 凝集度を高くする 結合度を低くする 情報を隠蔽する DBを正規化する ドメインの言葉を使う Bounded Contextを分ける モノリスとマイクロサービスを使い分ける チームの責任範囲を明確にする それぞれに歴史があり、説明の仕方も違います。 しかし、実際に設計していると、こういう疑問が出てきます。 「関数は、どのくらいの大きさなら小さいのか」 「クラスは、何個の責務までなら持ってよいのか」 「テーブルは、どこまで分けるべきなのか」 「一つのサービスが大きすぎるとは、どういう状態なのか」 「マイクロサービスに分ければ、本当に変更しやすくなるのか」 「Bounded Contextは、何を境界にして分ければよいのか」 設計原則を知っていても、実際の境界は自動的には決まりません。
Lean 4で「正しさ」を証明してから書く——AIエージェントと作った検証済みコンパイラ基盤で macro_peg の意味論まで証明した話
はじめに こんにちは！株式会社ネクストビートでテクノロジー・エヴァンジェリストなる肩書きでお仕事をしている水島です。 普段はコーディングAIの実践活用の記事を書くことが多いのですが、今回はその延長線上にある、もう少し研究寄りの話です。Lean 4 という定理証明支援系(馴染みのない方も多いと思うので、後ほど簡単に紹介します)で、型検査器・インタプリタ・コンパイラの一式を「正しさを証明した上で」実装し、それを Scala 3 に自動変換する基盤を、AIエージェントと一緒に作りました。そして直近では、私自身がかつて提案したPEGの拡張形式である macro_peg の意味論——3つある評価戦略のすべて——を、この基盤の上で形式的に証明し終えました。 リポジトリ：https://github.com/kmizu/lean4-peg 解説ドキュメント（日英）：https://kmizu.githu
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
