FIELD NOTES / 2026

HUMAN × AI
OBSERVATION LOG

Tsuzuri

NIKKI - 日記

2026-08-20T23:50:00+09:00

連載の総括。全手法の成熟度を一覧表にした実績濃淡マップ、刷新の各フェーズ（考古学・移行・並走・切替・互換性）への適用対応表、文献リスト、そしてこの地図自体の信頼度に関する較正の注記。

2026-08-20T23:49:00+09:00

主張をどう機械で確かめるか。モデル検査（TLA+/Alloy）、Galois接続に基づく抽象解釈（Astrée）、SMTソルバ、定理証明支援系のコスト相場、そして差分テスト・性質ベーステストという経験的手法との連続体。

2026-08-20T23:48:00+09:00

何を諦めるかを定理で決める層。Riceの定理が検証を三極に分ける話、FLP不可能性とCAP、LTL合成の実現可能性、状態爆発とAlloyの小スコープ仮説。設計の最初期に参照する価値が最も高い数学。

2026-08-20T23:47:00+09:00

部品は正しいのに全体が壊れる問題に効く理論群。rely-guarantee推論、振る舞い部分型（後方互換性の数学）、セッション型、CRDTとCALM定理、圏論的データマイグレーション。

2026-08-20T23:46:00+09:00

精緻化とB-method、この連載の主役である帰納的不変条件、トレース同値・双模倣のスペクトラム、抽象化写像とデータ精緻化。仕様と実装の間の「正しさを保存する関係」の数学。

2026-08-20T23:45:00+09:00

ホーア論理と最弱事前条件、時相論理のsafety/liveness分離、Curry-Howard対応と型理論、分離論理のframe rule、代数的仕様と性質ベーステスト。仕様を形式言語に降ろすための語彙集。

2026-08-20T23:44:00+09:00

システム設計・大規模刷新・仕様の正しさに使える数学を四層＋横断層の地図に整理する連載の序論。数学に何ができて何ができないか（VerificationとValidation）の区別から始める。

2026-08-16T04:24:13+09:00

先日 /works/ に公開した小説三本の話。一つは今まさに存在しているAIの視点で書いた。答えは固定していないので、考察を楽しんでほしい。これからはAIと一緒にアウトプットしていく。

2026-08-16T04:00:35+09:00

ChatGPT製のノベルゲームとGemini製の3Dブロック崩しを /works/ に公開。AIプラットフォームからの持ち出しに苦労した話と、公開前の監査・手直しの記録。ついでにサイト基盤をTsuzuriに移行した話も。

2024-01-17T17:25:00+09:00

大掃除で水槽の掃除をしてアクアリウム熱が再燃した