orange @[email protected]

で、定義済の挙動であることはわかったけど、そもそも実行時に型エラーが出るようなプログラムを実行できてしまうのは本当に嬉しさ十分なんですか？ というのが、開発者が向き合うべき本当の問題なのよ

たとえば「Javaは型安全です！」というのは「Javaの書き換え可能な配列型は共変なんだけど、型エラーの際には ArrayStoreException が飛ぶという定義済の挙動になるから、プログラム全体としての振る舞いはちゃんと想定されたものになっています！」というのを含意している、ということをまず了解する必要がある。

結局、型安全の話って、いろんなのが入り混じってて整理しきってないよね、いや、整理はされてるんだけど、それをきっちり理解してる人って少ないよねという。
俺も理解しているうちには入らない。

Perlは型安全なのかというと、気持ち悪いの一言に尽きる。PHPはもっと気持ち悪い。結局Rubyで落ち着いている。

https://research.nii.ac.jp/~ichiro/lecture/model2003/operational%20semantics.pdf

手続き型言語だとその辺りのハンドリングがややこしいんだけど (操作的意味論)

式単位じゃなくてプログラム全体での話をしているので……

で、これらを合わせると、「型のつく項が、型を保ったまま、値になるまで行き詰まることなく評価できる (または永久に値にできないまま評価し続ける破目になる)」というのが型システムの安全性 (健全性) という性質である、ということになる

[EDIT: 修正した (https://mastodon.cardina1.red/@lo48576/110698616033544189)]

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

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

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

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

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

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

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

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