orange @[email protected]

形式検証と契約プログラミングって、型のデザインが過度に複雑にならずに安全性を高められるって点でも、むしろ初学者に優しくなるかも＞＜

完全に型のみに頼れば、たとえば引数が0では無い整数である必要がある時には、『0では無い整数型』が必要になるし、結局どこかでその型への明示的な(あるいは暗黙の)型変換が必要になる＞＜

でも、怠慢なプログラマは、ゼロになっていないかのチェックを事前に行わずに、型変換時のエラーに任せるコードを書いちゃって、実行時にエラーが出るか、または出ないけどロジック的には誤りになるコードを記述してしまい、わざわざ『0では無い整数型』を導入したメリットがほとんど無くなっちゃう＞＜

形式検証であれば、実際のロジック部分(？)で「ゼロになる可能性があるのでその対策が必要なこと」をエラーまたはアドバイスにすることができ、
オプショナルで無視するつもりなら無視しておいて実行時のエラーに任せるという選択も出来て、同じ無視する場合でも型で記述する方式と比べると無駄な型変換コードが節約できる＞＜
そういう面でも初学者に易しいかも＞＜

Geminiとこれを土台に議論したけど、Geminiは「形式検証って学習曲線がつらいかし、やっぱミッションクリティカル向けでは？」って反論してきて、
それに「むしろミッションクリティカルな環境以外ではオプショナルな導入で十分で『書きたい人が必要な部分にのみ』ってスタイルで良さそうだし、なにより形式検証によるエラーメッセージは初学者に対して優しいヒントになるんでは？＞＜」ってなって、
Geminiが「たしかにそういう発想でのオプショナルな導入であればかなり有用だし、初学者のアシストとしての形式検証環境ってコンセプトは新しいかも！」(意訳)
ってなった＞＜(実際はもっと長い議論です)

なんで、AdaでしかSPARKというか、契約プログラミングを土台にした形式検証プログラミングが全く流行らないんだろう・・・＞＜
C#とか構文的にも静的検査の環境が充実してる点でも向いてるだろうし、Rustとかの安全を売りにしてる環境向けにもあってよさそうなのに＞＜
10年前とかのプログラマが使うPCでは、契約プログラミングの検査は遅かったけど、いま時のPCなら全然遅くないし、昔と違ってコード記述中にIDEがバックグラウンドで構文検査するのが当たり前になりつつあるわけだから、静的検査の時間によるストレスもほぼ無いだろうし・・・＞＜

(Adaの)SPARKって、SPARK 1990とSPARK 2014で、目的は同じでもかなり違うのか・・・＞＜
SPARK 1990ではジェネリックプログラミングも明確に禁止してたのか＞＜

自身より圧倒的に開発がアクティブで現役のソフトウェアとの通信機能を削除って酷い＞＜；

SPARK—an annotated Ada subset for safety-critical programming | Proceedings of the conference on TRI-ADA '90
https://dl.acm.org/doi/10.1145/255471.255563
https://doi.org/10.1145/255471.255563

何も言えないの表現に"「」"を使うのも、わりと老人会な気がしてる＞＜

オレンジはその（）を今も最大級の嘲笑に使ってる＞＜；

2chでも、2000年ごろ（？）とかは全然嘲笑じゃなかった気がする＞＜
2002年辺りでも煽ってる感じじゃなく、むしろ煽る時は（笑）ってわざわざ書く人の方が多かったような記憶ある＞＜（あやふや）

正確に言うと、あのゲームって奴隷制度の時代と、それが終わってから公民権運動までの約100年の強烈な人種差別の時代の両方をセットで追体験させるのが主軸っぽいので、わりととんでもなく強烈なゲームだよね＞＜
クリア後の選択も（一部の）優しい奴隷主の追体験だろうし＞＜