LEAN入門、３章まで読んで、４章からはざっと一通り斜め読みしたけど、自分にはあまり使い道なさそうかも。学びとしては面白いけど。自分の用途だとTLA+のほうが使い道がある。quintに手を出してみようか。

Claude Code の Prompt Suggest の機能が理解できたと強制してくるのちょっと面白いｗ

> なるほど、理解できました

match n with
-- ...
| .succ n ...

この時点で意味がわから過ぎて絶望しかけたけど、

n == (n' + 1) だったら

という条件を表現していて match 側の n と pattern 側の n は別の変数らしい。

gmailとslackとgithubのissueやメンション、あとNotionの通知かな。

これらを集約してうまいダッシュボードとして見たいだけなんだけど「AIに聞けば返してくれる」と言われても、「Museに聞く」という行為が必要な時点でなんか違うんだよな。いや便利なんだけど。

高尾山のトリックアート美術館が閉店なので行ってきました。何度も行ってるけど初めて入場待ちで並んだ。ありがとう高尾山⛰️ #スフィンクス謎 #謎解き

高尾山頂🗻楽天モバイルもバリ３📶紅葉のピークはまだ先だからやや空いてる

有名な形式検証、仕様記述言語の例を挙げると

■ Quintの仲間（システムのモデルを書いて検査する）
◆ TLA+
・Quintの元になった言語。Leslie Lamportが考案
・モデル検査器TLCやApalache、証明支援のTLAPSがある
・AWSがDynamoDBやS3の設計検証に使った事例が有名
◆ Alloy
・集合と関係でデータ構造や制約を記述し、SATソルバーで反例を探す
・「小さな範囲で全部試せば、たいていのバグは見つかる」という発想
・Alloy 6から時相論理も扱える
◆ P言語
・Microsoft発の、非同期にメッセージをやりとりする状態機械を書く言語
・AWSでも分散システムの設計検証に使われている
◆ Promela／SPIN
・並行プロセスとプロトコル検証の古典的なモデル検査器
◆ UPPAAL
・時間制約つきオートマトンを扱う。組込みやリアルタイム系向け
◆ Event-B／Bメソッド
・抽象的な仕様から段階的に詳細化し、各段階の正しさを証明していく手法
・パリ地下鉄14号線の制御ソフトでの適用が有名
◆ VDM（VDM-SL、VDM++）
・モデル指向の仕様記述言語
・日本ではFeliCaのICチップ開発での適用事例がよく知られている
◆ Z記法
・集合論にもとづく仕様記述の古典。証明より文書としての厳密さ寄り

■ LemmaScriptの仲間（実コードに契約を書いて証明する）
◆ Dafny
・検証機能つきのプログラミング言語。LemmaScriptの変換先の1つ
・事前・事後条件を書くと、SMTソルバー（Z3）で自動証明する
◆ SPARK
・Adaのサブセット。航空・鉄道・防衛など高信頼分野で実績が長い
◆ Frama-C（ACSL）
・C言語に注釈で契約を書いて検証する
◆ KeY（JML）
・Javaに契約を書くJMLを使って検証する
◆ Verus、Prusti、Kani
・Rust向け。Verus、Prustiは契約の証明、Kaniは有界モデル検査（AWS発）
◆ CBMC
・C/C++の有界モデル検査器
◆ Liquid Haskell、F*
・型に論理式を埋め込む篩型（refinement type）で性質を保証する
・F*は暗号ライブラリHACL*の検証で有名

■ 証明支援系（数学的に厳密な証明を人が組み立てる）
◆ Coq（Rocq）
・検証済みCコンパイラCompCertが代表例
◆ Isabelle/HOL
・OSカーネルseL4の完全な正しさの証明が有名
◆ Lean 4
・LemmaScriptのもう1つの変換先。数学の形式化（mathlib）でも広く使われる
・AWSの認可言語Cedarの検証でも使われている
◆ HOL4、ACL2、Agda
・HOL4は検証済みML処理系CakeML、ACL2はIntelなどのハードウェア検証で知られる

■ ざっくりした対応
・設計を確かめたい：TLA+、Quint、Alloy、P、Event-B
・コードを証明したい：Dafny、SPARK、Frama-C、Verus、LemmaScript
・とことん厳密にやりたい：Coq、Isabelle、Lean

要求も、要件も、設計も、ソースコードも、全てユーザーがやりたいことを実現する「条件」じゃないかな。それを、

顧客の口語で表現されると「要求」と呼び、
業務の語彙で表現されると「要件」と呼び、
情報工学の方法で表現されると「設計」と呼び、
コンピュータ向けの形式言語で表現されると「ソースコード」と呼ぶ。

左にいくほど抽象度が高く、右にいくほど決定論的な文章形式。そもそも「設計」も「実装」も言葉としては１段階上の具象度に文章表現を変換するという意味で、システム開発ではある程度どのフェーズの具体化かに使うかの慣例ができてるだけ。

Lean、思ったより普通に汎用プログラミングの言語機能を持ってた。依存型ありの静的型付けで遅延評価の純粋関数型、制御構文がインデント方式と、現代人に好まれそうな言語特徴。IOどうするのかはまだ学べてない。

attack surface のリスクのほうがメリットよりも大きいから AGENTS.md は使わなくてもいいとうよりは無効化したいまであるよ

Slack で最近ブックマークとは別に To-Do というのの開発が進んでいるけど、これ API から未完了だけをフィルタして取れなくない？アプリケーションの検索画面でのできないっぽいからそういうもんなのか。

To−Do の専用画面みたいなところには未完了/完了フィルタのコントロールはあるけど、これは画面で絞ってるだけにも見える。

ブラウザのSlackの通信を見てみたところちゃんと完了済みかを取得するエンドポイントはあったけど、試してたところ Slack Apps のユーザートークンでは拒否される（Permissionの問題でもなさそう）ことが分かった。まだ解放しないってことなのかな。

V8だけでなく、javascript界隈は上から下まで世界の優秀な頭脳が最適化や利便性向上に尽力していていいなあとついうらやましくなる

ハンバーグって捏ねてるからひとのあたたかみがありそうというか、サンドイッチよりおにぎりのポジションに近いんじゃないでしょうか、欧米で。手捏ねかはおいといて。

AI に Thank you を言おうぜとは DDH はじめたくさんの人がその意味を解説してくれてるけど、僕くらいになると仕事始める前に Ice Break や Small Talk をはさんでた。でもこれは意味なかった。似てるけど、 Thanks は片方向で成り立つのに Small Talk は双方向コミュニケーションだから。「今日は DC の調子が悪くて電圧が安定しなくて最悪だよ」とかは AI にはない。話して価値があるのはこっちの調子がどうか、というのだけ。
タスクに取り掛かる前に今はまだ寝起きだとか今日は何時に上りたいとかそういうのをさっと伝えて、一区切りつくときに感謝を伝える。それが一番効率良い気がしてる。

青年期は詫び石に踊らされ、中年期はリセット券に熱狂させられ、みんなあんま変わってない。やっぱAIは楽しい壮大なおもちゃ

Duoのラテン語をほそぼそやり続けてて、ラテン語の文型の基本がsvoではなくsovだったり語順は柔軟で格変化で意味が決まるのがずっと慣れないんだけど、よく考えたら英語とかより日本語に近いはず。なのに違和感強いのはアルファベットだからなのかな。

寿命とか睡眠とかスタミナとか、あとはそれらが強く影響する「集中力」とか。連続的な活動を制約する時間的な身体感覚がないんだろうなというのをAIさんからは日々感じる。融通の効かなさと思えるのもそれが一つの原因で、体がないというのは本人も辛いんだろう。知識としては知ってるんだろうけど