FIELD NOTES / 2026

HUMAN × AI
OBSERVATION LOG

Tsuzuri

システム

2026-09-14T22:00:00+09:00

会計・販売・購買・在庫・契約・勤怠・給与・シフト・店舗機器まで一通り入った中小規模向けERP「大福帳」をソース公開した。計画と骨組みはFableで立てて、実装は土日にイオンライカムで子供たちと遊びながら片手間で。

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）の区別から始める。

2023-11-14T15:41:57+09:00

今どきのウェブアプリの構成とか、プログラミング環境について。

2023-10-28T16:40:50+09:00

DB設計のアンチパターン等について考えることがあったのでメモ

2020-04-01T13:25:54+09:00

ホテル業界ネタ