型安全ってなんだろう?

よくわからないのでツイートしたらアドバイスもらえました。
22
Jun Furuse 🐫🌴 @camloeba

@kyon_mm 文字列をbooleanと混同したくない(普通の人が言ってる型安全)、配列外アクセスを排除したい、デッドロックが無いことを保証したい、機密情報漏れが無いことを保証したいなどなど。ありとあらゆる安全性の基準がありそれをプログラムを抽象的に捉えた型というもので抑えたい

2012-09-20 19:45:48
mzp @mzp

念のためTAPLひっぱりだしてきたけど、Type safetyには"see safety"と書いてあって、Safety = Progress + Preservationと定義されてた。

2012-09-20 19:45:50
mzp @mzp

Type Safety: 型がつくなら値になる、かつ、簡約してる途中で型が変わらない

2012-09-20 19:47:08
Jun Furuse 🐫🌴 @camloeba

@mzp 確かに presevation がなかったら困るw

2012-09-20 19:48:52
Jun Furuse 🐫🌴 @camloeba

今望まれてるのは型がついてれば俺の昇給が保証されてるような型安全性

2012-09-20 19:50:16
きょん@アジャイルコーチ、システムアーキテクト @kyon_mm

@camloeba あー。。。なるほど。そう考えると、関数型界隈?で語られることが多いのは、内部設計的な何かの集合を型で表現しようという試みなのでしょうか?それをより外部設計的な方向に持って行こうとするのがカリーハワード対応?

2012-09-20 19:51:13
Hideyuki Tanaka @tanakh

( ˘⊖˘) 。o(絶対に損害が出ないトレードを行う型的なのを作っているのかなあ…)

2012-09-20 19:51:55