orange @[email protected]

保存: 項 t に型がついて t が項 t' へと評価できるなら、 t' には t と同じ型がつく。

ようは評価してたら急に型が変わったりしないという話

進行: 項 t に型がつくなら、 t は値であるか、または別の項へと評価できる。

項ってのは大雑把には「式」みたいな概念だと思っといていいかも

TAPL を参照するなら §8.3『安全性 = 進行 + 保存』がドンピシャの節か？

算術式がメモリを破壊するとかしないとか、そういう考え方はしない。

チューリング機械は計算機のいち実装でしかない

そもそも一般的な「計算」をメモリと CPU とかいう限定的なアーキテクチャで考えない

そもそもメモリ破壊とかを持ち出すのがレイヤー違いという感じがする (たとえば単純な項書換え系の言語を考えたときメモリ破壊もクソもない)

型安全はどうでもいいから、振る舞いの滅茶苦茶さと記述の気持ち悪さをどうにかしてくれ、みたいな方。とはいえ、振る舞いの滅茶苦茶さの中に、勝手に型変換するよ～、便利でしょ？？みたいなのも入ってるのかもしれん。

人々は型安全なプログラムを書きたいわけではなく振る舞いの良いプログラムを書きたいのだから

うんちみたいな動作するけど型安全だよ！ というのがアリで、それを了解できるなら、それ以上型安全であることそのものを論じたってに実際的は嬉しくないでしょ (理論的なあれこれはさておき)

つまり意味論から逃げるなということなんだけど

それはそうで、同時に「狭義型安全かどうか」そのものの有難味の本質に目を向けろという話なんだよな