orange @[email protected]

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年の強烈な人種差別の時代の両方をセットで追体験させるのが主軸っぽいので、わりととんでもなく強烈なゲームだよね＞＜
クリア後の選択も（一部の）優しい奴隷主の追体験だろうし＞＜

Detroit: Become Human、たぶん地下鉄道を知らずにプレイしてから、現実のアメリカの奴隷制度の時代がそういう感じだったって知る方が衝撃大きそうだし、いい意味でシリアスゲーム効果（？）が高そう＞＜

Detroit: Become Humanも、モチーフにしてる黒人差別と地下鉄道（アメリカの奴隷制度末期の奴隷解放ネットワーク）等などを知っててストーリーを見る（体験する）のと知らないで見るのでは全然感覚違いそうだし、知らずに見る方が「差別はよくない」って感情を強く持ちそうな気がする＞＜