Rustって新しい言語だ。あっという間に人気が出た。といっても、メジャーではない。新規の言語としては人気がある。といっても、マニア層な気もする。
Web Assemblyとかライブラリやインフラの開発も早いようだ。
簡潔。
Rustは何が新しいのか（基本的な言語機能の紹介） - いもす研 (imos laboratory)
大学の先生の書籍。ポイントを抑えている。リファレンスとしては不足な印象だ。
言語マニアによる書籍だ。読んでみたい。まだ。大きい本。字は小さい。
モチベーションになる。作りたい題材として。
ぜんぜん勉強しないので、資料を集めてみる。
読んでいって、わかりやすい順にソートします。
【図解】Dockerの全体像を理解する -前編- - Qiita
簡潔でよさそう。
【触って理解！】Docker入門 - 初心者に向けて使い方や基本コマンドを解説 | IT・ものづくりエンジニアの転職・派遣求人情報なら【パソナテック】
Dockerのことが多分わかるハンズオン - Speaker Deck
途中でRailsの事例になって、知らんので、ぽかーん
Docker入門（第一回）～Dockerとは何か、何が良いのか～ | さくらのナレッジ
あとGitもわからへん
下記をちょっとF#で書いてみる。
あれ、編集距離と違うのかな？
open System let rec editDistance (s1:char list) (s2:char list) : int = match (s1, s2) with | ([], _) -> Seq.length s2 | (_, []) -> Seq.length s1 | (h1::t1, h2::t2) -> if h1 = h2 then editDistance t1 t2 else 1 + List.min [ editDistance t1 s2; editDistance s1 t2; editDistance t1 t2] let ed (s1:string) (s2:string) = editDistance (Seq.toList s1) (Seq.toList s2) [<EntryPoint>] let main argv = printfn "Hello World from F#!" printfn "%d" <| ed "" "tesat" 0 // return an integer exit code
ツールはよくわからない。独自？
Amazon S3の軽量形式手法 - masateruk’s blog
Spin
3．形式手法を応用した、仕様段階でのバグの検出 a．形式手法（Spin／Promela等）を利用し、仕様の形式記述言語を表現し、仕様バグを早期に発見する b．形式記述言語支援ツールの開発
プログラマー | 株式会社ディー･エヌ･エーの求人詳細 | ゲーム業界の転職・求人情報なら ファミキャリ！ - ファミ通.com
DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました（録画・スライドあり） - DeNA Testing Blog
なかなかいいな。就職するには、会社の業績も気になるところ。業績悪化で、型式手法の適用中止になったら、詰むよね。 まあ、日本で型式手法が必須な産業はあるのか知りません。適用したらもとが取れる分野はあると信じたい。
Coq
Heartbleedが公開されたときに、どのようにして次のバグを防ぐかが話題になっていました。ユニットテストを使うとか、各種アナライザーツールで検査するとか、フォークして綺麗に書き直してみるとか、APIも悪いとか、mallocを自作してはいけないとか、C言語はよくないから他の言語を使うべきとかいろいろありました。
他の言語の候補としてはATSが人気のようでしたが、自分の使い慣れているCoqでTLS/SSLを実装するとどうなるか考えていました。 プロトコルの安全性の証明などは大変ですし、実装の安全性にはたいして寄与しないので、見ただけで正しい実装をしているとすぐに確認できる程度のものを作ることを考えていました。
CCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介｜レピダム
株式会社フォーマルテックは形式手法の普及拡大を目指すモデル検査の専門企業です。
よくわからないですが、、
【具体的な業務内容】 組込みソフトウェア開発の （１）プロセス改善 （２）アーキテクチャ開発／改善 （３）形式手法の導入 などに従事していただきます。
組込みソフトウェアコンサルタント | イーソル 株式会社 | IT/Web業界の求人・採用情報に強い転職サイトGreen(グリーン) | 2009/07/30 21:04:00更新 | id:8056
やっぱりモナドわすれるな（わかっていない？）と思って、時間ができたのでReal World Haskell読もうかなあ。
と思いつつ、
積ん読のこちらを思い出し、『プログラミングHaskell第２版』Graham Hutton 著、山本和彦 訳を読む。
Functor、Applicativeからの流れのあとのMonadの説明がわかりやすい。というか簡潔で、この導入がいいんじゃないかと。Real World Haskellは違った導入だった気がする。
しかし、以下のブログを読んでしまった。
具体的には、関手（ファンクター）→アプリカティブ→モナドという解説の流れは、この本が作り出しました。 この説明の流れは、「同じパターンで定義できる関数」をHaskellでどのようにまとめるかについて、『Real World Haskell』のころには知られていなかった知見を反映したものです。
なんと『すごいHaskellたのしく学ぼう！』でもその流れの説明だったとか。既読だったんですよ、数年前にね（ｗ）
RWH読み返している場合じゃなかった。
要点は、あいまいに以下記載する。
Functorはコンテナみたいなデータ構造（IOも）の中身に関する純粋関数適用。
Applicativeはその一般化で、複数引数OKに一般化する。ここで作用とかでてきて、作用は引数だけが対象。なんだか書いててよくわからない。引数を適用していく過程に作用がある。あくまで適用できるのは純粋関数適用（作用なしの関数の適用）。pureなんかそれかな。
Monadは純粋関数でなく作用のある関数の適用に拡張されている。純粋関数だけじゃなくて。a->Maybe bみたいな関数のフレームワークなんだよ。いきなりフレームワークってなんだよ？ってところだが、計算戦略みたいなものだろうか。適用なのかもしれない。bindでつないだりすることかな。Applicativeだって<*>ってつなぐアレ。
TreeのカウントアップしたLeafをつくっていうのはStateモナドを使用して、あーなるほど、と思うんだよ。これってYesodでHTML構成するときの記法だやな、これだったのかな、Stateモナド（かReaderか Writer）みたいなデータを引き回しているんだろうな、きっと。
そういえばStateモナドの図はこの本がわかりやすいべ。
仕事にて、つかれ過ぎてて、メモる裏紙。
パワハラ、過労事例をメモります。
大企業や官公庁だって、パワハラや過労を防げていない現状があります。
この社会はまだ進歩する必要があるのです。
隠蔽には７人が関与していた。社内調査に対し、総務部門の係長は「遺族に労災の疑いをかけられたくなく、事実と異なる回答をしてしまった」と釈明。労政企画部長や法務担当らも「『すでに遺族に回答しており、もう引き返すことは難しい』という係長の主張を追認してしまった」などと話したという。同社は１６年８月、係長ら４人を降格、労政企画部長や法務担当ら３人を停職１０日の懲戒処分とした。
同社は遺族に対し、パソコンの履歴や同僚らの証言から、男性が就業時間以外の夜間や休日に仕事をしていた事実を認めた。一方で同社は、残業や会社外での業務は指示しておらず、勤怠管理に違法性や不適切な点もなかったとし、労基署も労災とは認めなかった。
同社は読売新聞の取材に「すでにご遺族の方々と円満な解決をしているため、コメントは差し控える」とした。
【独自】自殺社員のＰＣ隠蔽、遺族に「廃棄」と説明…ホンダが７人懲戒処分 : 社会 : ニュース : 読売新聞オンライン
こういうとき円満な解決という言葉を使用するのか？
パワハラ被害を受けた男性は、東京大学大学院を修了後、15年4月に入社。配属された部署で、直属の上司から「ばか、アホ」「こんな説明ができないなら死んだ方がいい」などと繰り返し言われ、個室に呼ばれた際には「発言を録音してないだろうな。携帯電話を出せ」と言われたそうです。
男性はその後、適応障害と診断され休職し、16年10月に別の上司の下で復職。しかし、仕事で重圧がかかると手が震えるなどの状況が続き、17年7月には両親に、「会社ってごみや、死んだ方がましや」とメールを送り、周囲にも「自殺するかもしれない。ロープを買った」「死んで楽になりたい」などと漏らしていました。
そして、17年10月末、寮の自室で自殺。豊田労働基準監督署は19年9月、パワハラと自殺の因果関係を認め労災認定し、21年4月にトヨタと遺族側で和解が成立しました。
トヨタは「人間の顔をした会社」に変われるか？ 「パワハラ再発防止策」を読み解く：河合薫の「社会を蝕む“ジジイの壁”- ITmedia ビジネスオンライン
パワハラを適応障害になるまで防げなくて、復職後も周囲に苦境を話していたのに、自殺を防げないのか。
直属の上司に問題がある場合、他に相談する窓口があるべきで、すでにあったようだが、この件に関しては機能しなかったのだろう。
メンタルに配慮しなかった会社の責任を認める - 過労死、過労自殺にとりくむ弁護士 岩井羊一法律事務所
この事件は、デンソーの社員である原告が、トヨタ自動車へ１９９９年８月に出向したのちに２０００年４月ころうつ病を発症し、８月に休職。いったん回復し、デンソーに復職したが、２００２年６月ころからのデンソーとトヨタ自動車の共同のプロジェクトのなかで、うつ病を再発。現在も治療しながら在職しているという事案です。
デンソー、トヨタ自動車の業務が原因でうつ病になり、休職を余儀なくされたことについて、デンソー、トヨタ自動車の責任を問い、損害として発生した休業損害、逸失利益、慰謝料など請求していました。 判決は、「被告デンソーは、平成１１年１１月には、原告に対し、業務の軽減、その他何らかの援助を与えるべき義務が生じ、その後も原告の業務遂行の状況や健康状態に注意し、援助を与える義務があったというべきであり、それにもかかわらず、少なくとも原告が第１回うつを発症するまでこれを怠り、また、遅くとも平成１２年３月には被告デンソーに帰社させるべきであったのに、かえって長期出張をしたのであるから、同義務の不履行がある。」としてデンソーの安全配慮義務違反を認めています。
また、判決は「平成１１年１２月、（中略）被告トヨタは、原告に対し、業務の軽減、そのほか何らかの援助を与えるべき義務が生じ、その後も、原告の業務遂行の状況や健康状態に注意し、援助を与える義務があったというべきであり、それにもかかわらず、少なくとも原告が第１回うつを発病するまでこれを怠っていたのであるから、同義務の不履行がある。」としてトヨタ自動車の安全配慮義務違反も認めています。 判決は、これらの安全配慮義務違反を認めて、休業損害、慰謝料を支払うように命じました。
うつ病により休職した。その後、健康状態に注意する必要があったのに、かえって長期出張をさせた等の問題です。
トヨタ自動車とデンソーという会社の間の力関係も、関係していそうです。
判決については以下のコメントがあります。
ここでは、平均的労働者には精神障害等の疾患が発症しないような過重な業務があった場合にも、予見可能性があった場合には，被告の責任があると認めているところに意義があります。本件にこのような基準を当てはめて原告を平均的労働者より脆弱だと認定したことには不満がありますが、一般論としては興味深い判断です。
三菱電機｢8年で自殺5人｣何とも異常すぎる職場 | 最新の週刊東洋経済 | 東洋経済オンライン | 社会をよくする経済ニュース
上は2020年の記事。
2017年にはホワイト500に認定。
当社は、経済産業省の健康経営優良法人認定制度において、2017年度大規模法人部門（ホワイト500）の認定を受けました。今後も、従業員が安心して働くことができる、安全・健康・快適な職場づくりに積極的に取り組んでいきます。
2021年もか。
三菱電機は、健康経営に資する各種活動が評価され、経済産業省と日本健康会議により「健康経営優良法人2021（大規模法人部門（ホワイト500））」として認定されました。
まあ年度ごとに認定ということでしょうか、ホワイト500。
技術系社員が相次いで労災認定されていた三菱電機で、主要電機各社の中で最長水準の残業が常態化していたことが、電機各社の労働組合でつくる電機連合の調査でわかった。
事務系はほぼ０だろうから、技術系はもっと長いって話です。
過労死｢31歳NHK記者｣を追いつめた選挙取材の闇 | 未和 NHK記者の死が問いかけるもの | 東洋経済オンライン | 社会をよくする経済ニュース
電通「過労自殺」事件から5年 “命を削る働き方”がはびこる社会は変わったか：河合薫の「社会を蝕む“ジジイの壁”」（1/4 ページ） - ITmedia ビジネスオンライン
東芝子会社社員の過労自殺も労災認定、三菱電機だけではない「理系職場の悲劇」 | Diamond Premium News | ダイヤモンド・オンライン
中央官庁も問題。地方役所は、個人に荷重がかかり、耐性が無いため実は問題が発生しやすいのではないだろうか。
休みたいのでうつ病と診断してほしい、などの話もあるようです。
でも、休みたいという切実な状況と、本当のうつ病の判別はつくのだろうか？ これは難しい問題と思います。
https://m.newsweekjapan.jp/stories/world/2017/07/---7_1.phpm.newsweekjapan.jp
自分も病気ではないんだろうか。単なる労務問題なんだろうか。
診断書に頼らず、相談できる機関はどこだろう？
よくある話のようにも思えるが、これも奥田氏によれば典型的な「社会的うつ」だという。
「この男性の場合、自分から精神科に行っていますが、その理由が週刊誌の記事にあった『うつ病チェックリスト』に自覚症状の一部が当てはまったからというものです。これは近年のメディアの問題ですが、うつ病を誰でも罹る病気として報道することで『大衆化』し、受診するハードルを下げすぎる傾向にあります。本来この方がやるべきだったのは、会社に職場の過重労働の問題を訴えて仕事量を調整することだったはずです。最悪の場合、復職しても精神疾患のレッテルを貼られて窓際に追いやられ、まともに仕事をさせてもらえない可能性すらあるでしょう」
大きい会社でもパワハラ、過労死を防げない21世紀のようです。
ましてや中小では…
困ったら逃げなきゃね、 と思います。
現職（C）が辛くて、ほんとは関数型言語とかやりたかったんだよね。
HERP TechHub | TypeScript,Haskell,Node.jsをはじめとして、HERPで使用されている技術にまつわるメンバーブログへのHub
中の人の記事。
Elm
Idein Ideas — Elm で快適なフロントエンド開発
なかに強そうな人がいそう。
About | κeenのHappy Hacκing Blog
弊社エンジニアが出版に関係した書籍例 • 関数プログラミング入門 • 実践Rust入門 • Elm本 • 型システム入門 • プログラミングGauche • Real World Haskell • Haskell Relational Record • 抽象によるソフトウェア設計
Idein Inc. 会社紹介資料（July. 2020）（Idein株式会社）のカタログ無料ダウンロード｜製造業向けカタログポータル Aperza Catalog（アペルザカタログ）
ここが詳しい。
私の仕事もそういう文脈からきていて、例えばニューラルネットをコンパイルしてRasp PiのGPUで動かすだとか、あるいはもうちょっと特化したデバイス（ぼかしてる）のためのコンパイラを作るだとかの仕事になります。 自分で書いておきながらやっぱり「ニューラルネットをコンパイルする」っていう字面がパワーある。 今、（学習ではなくて予測に）使われているのはほとんどがモデルと実行器が分けらています。要はインタプリタなのでそれをコンパイルしてあげて高速に実行するというのが可能なんですね。 ニューラルネットの圧縮のために数学が必要そうな雰囲気で、数学出来ない私は震え上がってます。
Idein Incに入社しました | κeenのHappy Hacκing Blog
Elm
Coq、OCaml
中の人が業務でCoqを使って見つけたのかな？
CCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介｜レピダム
定理証明支援系によるソフトウェア検証
とあるので、Coq使っていそうだな。あと、モデルチェッカとか。
Erlang/OTP
おっ
過去最高の売上だった前期を超えました、それも大幅に。自社製品の売上割合も上がりました。今期も前期を上回る賞与で 1 人 1000 万円以上の予定です。
おっ
時雨堂の正社員に向いていない人
大人として働けない人
お金を稼ぎたい人
技術にこだわりすぎる人
朝起きられない人
Elm
こんなリストが、、
システムエンジニア《自社勤務/東証一部上場》 - 東京都 中央区 銀座 - Indeed.com
継続しているかは不明系
情報お寄せください。
関数型プログラミングやっている人って、優秀にみえるので、
計算機に推論できる型、できない型 | Wantedly Engineer Blog
けっこう技術のあるひと集めいているのかなって雰囲気あるわ、この記事のアイキャッチはTaPLかｗｗｗｗ
![実践Rust入門 [言語仕様から開発手法まで]](https://m.media-amazon.com/images/I/51t+hDKJOvL._SL500_.jpg "実践Rust入門 [言語仕様から開発手法まで]")
