！＞＜
-- Undo & Redo https://support.gitkraken.com/working-with-commits/undo-and-redo/
！＞＜
-- Undo & Redo https://support.gitkraken.com/working-with-commits/undo-and-redo/
・・・と思いながら、200万円以下の古いクルマってどんなのあるだろう？＞＜ってカーセンサー見てたら、EVコンバートされてるダルマセリカ見つけた＞＜；
https://www.carsensor.net/usedcar/detail/CU4397523877/index.html?TRCD=200002
でも、200万円払うなら既に（スポーティーな）クルマが好きな人なら中古車の本格的なやつ（？）を買うよねたぶん・・・＞＜
一応各社だいたい、180万から200万円以下のホットモデルのような物はある事はあるっぽさ＞＜
（三菱は無い？＞＜ スバルはインプレッサが当てはまるのかどうか微妙な気がするけどスポーツって言ってるから（？）一応車種丸ごとそういう若い人狙い？＞＜ アルトワークスは150万円台だしすごい＞＜）
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
トヨタのGRってまさにクルマ離れの反省からのコンセプトだったはずだし、86も最初は（？）そうだったはずだけど、お値段も含めて結果的に小金持ちのおっさん向けっぽさが・・・＞＜
（イメージリーダーであればよいって事らしい？＞＜（でも、イメージリーダーでイメージできても（？）、イメージ持ったとして自分が乗れるクルマはどれ？となるとどうなのさ感＞＜））
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。
突然思いついたけど、通販でひざの曲げ伸ばしが楽な ひざサポーター？＞＜ってあるじゃん？＞＜ お年寄りとか向けのやつ＞＜
あれの、自転車用のむしろ足が強靭な人がより速く自転車漕げるようにするバージョンってないのかな？＞＜
なので、自動車メーカーが言ってる文脈での「若者のクルマ離れ」って、そういう所からメーカーが認識して危機感を持ってる話なので、雑誌とか新聞とかがてきとうに書くような（？）「若者の○○離れ」とはちょっと違う感じがあるっぽさ＞＜
クルマ売れる売れないじゃなく、実際に整備士になってる人々までもが（整備士になる前に）趣味的に興味を持ってもらえてなくてヤバい＞＜
で、若者のクルマ離れってマジ？って話で、整備士さんのうち「クルマが好きでなりました」って人がものすごく減ってる事が（メーカーが行う）研修なんかの（横断的に観察できる）場で目に見えてきて、よそのメーカーと話しても「うちもそう」みたいな感じで、「こりゃやばいぞ」となって色々（特にトヨタとか）若い人にクルマに趣味的に興味を持ってもらおうとがんばってる（？）かも＞＜
そういえば、クルマの整備士さんも、クルマ好きでなった人（オレンジの家族の人がそう）と、そうじゃなくてなった人が居て（そりゃいて当たり前だろうけど）、
好きでなった人の方がおもしろがって新型のクルマとか「電気自動車で整備はどう変わるのか？」とか研修とかも自発的にそれこそ趣味のように命令されずとも行ってどんどん学ぶんだけど、好きじゃないのになった人々はそれが無いので、なんかアレだ（駄目ではないけど）という＞＜
このアカウントは、notestockで公開設定になっていません。
雑に言うと、Haskellerがいう型システムだと「『リンゴが3つ』と『バナナが3つ』はこの場合は同じ」みたいな発想だけど、Ada的発想でいう型システムだと「まず果物にそろえよ！ そもそもバナナが3つってなんだ！？ 房か！？本数か！？質量か！？ 数え方と単位も明示せよ！」って感じかも？＞＜
前者だと現在の小学校の算数の教え方とあんまり変わらない・・・＞＜
Ada方式の方が小学校1年生くらい？での「1ってなに？ なんで1の次は2なの？」とか「おにぎり＋おにぎりはでっかいおにぎりじゃん！？ さんすうわけわからない さんすうきらい・・・」みたいなことを小学校で教えたり救ったりできるかも？＞＜
それを踏まえると単に「型システム」と言うと、Haskellerが思い浮かべる物を指す方がより正確（？）なんだろうけど、じゃあ『その応用でAdaみたくガチガチで頭堅くて「明示的！！明示的記述！！命名せよ！！！暗黙は人を殺すミスを犯す！！！」みたいな、型を書かせる事によって齟齬を検出する意味での型システム』ってなんて言うんだろ？＞＜
ていうか、Haskellとかその辺の型システム（以下『前者』）って、人間と計算機の間の齟齬を最小限にしつつも記述を簡潔にする為にあって、Adaとかそっち方面の型システムは、前者の応用で、人間と人間でも（もっと言うとあるひとりのプログラマ自身と自身でも）齟齬を起こさないために明示的に意思を毎回わざわざ確認する、ある種の意思決定システムなので、なんと言うか、数学と工学のようというか、理学と工学のような、基礎と応用（？）の関係みたいな違いがある？＞＜
この齟齬、Adaの発想の延長で「小学校の算数にも（Ada的発想の）型システムを！＞＜ そうすれば教えるの楽だろうし混乱しないかも＞＜」って言ってる意図は、Haskellerとかその辺の方々にはそのままだと通じない可能性？＞＜； ていうか、だからこそ数学界隈の方々は否定する？＞＜；
だから、オレンジには、Haskellが「型ありき！」「型ありき！」とかいいながら、
「なんで型推論多用するの？＞＜ プリミティブ型（？ 標準ライブラリの型）そのまま使うの？＞＜ それじゃ（ヒューマンエラーの観点から言うと）、型がゆるふわな言語と対して変わらないじゃん？＞＜」
と見えたのかも＞＜
でも、Haskellerの方々にしてみれば、弱い型つけの言語は自明ではない記述（？）が出来てしまう、Haskellのように十分に（？）強い型つけの言語であれば、記述は自明（？）になる（あるひとつの意味としか読むことが出来ない）ので、実用的に（型）安全であるということになるのかも？＞＜
Haskellとかがいう型ありきは、プログラム意味論とかで、推論や自明性（？）を活用して記述を楽する（？）為に型を使うみたいな感じ？＞＜
（めちゃくちゃ雑にいうとジェネリクスとかそういうのの超すごいやつ（？））
一方、Adaの型ありきは、それを元にむしろ制限させる事の為に、同じように抽象化できる物を、ヒューマンエラーを検出する為に明示的にのみ行わせると言う発想？＞＜
ていうか、
https://mstdn.nere9.help/@orange_in_space/101389196152287067
これ読んだ瞬間に
「Haskellは型ありきの発想で...」
「Adaみたいに型システムを活用してヒューマンエラーを検出する方が型ありきじゃん！？＞＜ 型作ってよ！＞＜ 型書いてよ！＞＜」
の間の齟齬がどういうことかやっとわかったかも＞＜
これ、どういう人が書いたのか全くわからず(情報系の先生なのは本文からわかるけど)、単にググって「おもしろいなるほど＞＜」 と思って読んでtootしてそして最後まで読んで、それからやっと「何の研究してる先生なんだろ？＞＜」とリンクをクリックして、ぞわっと来た＞＜
"インタラクティブメディア・ユーザーインタフェース・情報可視化・..."(以下略)
https://fukuchi.org/index.html.ja
読みかけだけどおもしろい＞＜(読みかけなのにtootするほどに＞＜)
-- プログラムを数学の言葉で理解すること https://fukuchi.org/essay/2015/math-or-machinecode.html
