#5 Эно нюрнэнало - ボクたちの言葉が忘れられるこの世界は間違っている（Fafs F. Sashimi） - カクヨム https://kakuyomu.jp/works/1177354054886810570/episodes/1177354054886832312

三良坂さん〇〇に操られているんじゃ……？（疑心暗鬼（いせにほ第3部エピローグの衝撃が抜けていない））

いせにほ第3部エピローグでKranteerl短期過剰摂取の後遺症がフラッシュバックして「三良坂さんが泊まりたがるのは〇〇に操られてるから、間違いない」以外の感想が出てこない

『ボクたちの言葉が忘れられるこの世界は間違っている』、略称がほしいところ

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

:don:指宿温泉オフ

私はオーストラリアでAustraliaキャップを買ったりスイスでSWISS MOUNTAINS Tシャツを買ったりするのでI LOVE TOKYOイブを笑えないんだよな

2te larfa : Lidysteineskosti - "Icekai" es xorln unde（@cashimi） - カクヨム https://kakuyomu.jp/works/1177354054886781008/episodes/1177354054886875454

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

（少女に付き従う巨大な男と対峙するおたきゅらいんさん）（例のポーズ）（特別エンディング映像）

アニメ化して唐突にオーバーエッジとかいう謎の設定が生えてきた（アニメスタッフが生やしたのかと思いきやきのこが大本だった（い　つ　も　の））のすき

ロシア宇宙主義 - Wikipedia https://ja.wikipedia.org/wiki/%E3%83%AD%E3%82%B7%E3%82%A2%E5%AE%87%E5%AE%99%E4%B8%BB%E7%BE%A9

ICARUS Neutrino Detector Installation at Fermilab https://youtu.be/1Qmr7WEKy-Q

このアカウントは、notestockで公開設定になっていません。

コードに問題がある場合もある（たとえば、世の中のC言語のコードにはしばしば言語仕様上動くことが保証されていない記述が含まれている）し、最適化にバグがある場合もあるし、強い最適化の中には言語仕様上許されていないコード変換を行うもの（GCCの-ffast-mathなど）もあって、これを使うと言語仕様によればある結果が確実に得られるコードも別の結果を得るようになって壊れることがある

最後の話についてもう少し話すと、数学の授業で習うa * (b + c) = a * b + a * cのような恒等式で表される式変形がプログラミング言語が提供している整数型や浮動小数点数型の式でも必ず成り立つとは限らないのですが、-ffast-mathのようなオプションはあたかも必ず成り立つかのように式変形をして計算を高速化する代わりに結果が元の式と別の値になったりならなかったりします

最初の話についてはコンパイラのバージョンを上げると壊れたり、コンパイラを変える（GCCからClangとか）と壊れたり、最適化レベルを上げると壊れたり、コンパイラのバージョンも最適化レベルも同じでも出力コードのCPUアーキテクチャが違うとアーキテクチャ依存の最適化パスが切り替わって壊れたり、ありとあらゆるタイミングで壊れる可能性があるのでUBはやめようねという話

このアカウントは、notestockで公開設定になっていません。

その通り

2番目の話についてはコンパイラにコントリビューションしよう以外に言うことがない

LLVM Project Blog: What Every C Programmer Should Know About Undefined Behavior #1/3 http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html

最初の話については（以前も紹介したけど）この3回シリーズを読むと良いよ

以前ここに貼ったけど、GCCとClangで最適化パスの適用順序が違うので、さっきの記事の2回目 http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html に登場するある順番で最適化するとNULLチェックが吹っ飛ぶけど別の順番で最適化するとNULLチェックが残るという例は実際に起きる

http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html の例はこれですね。

void contains_null_check(int *P) {
　int dead = *P;
　if (P == 0) return;
　*P = 4;
}

このコードに「不要なNULLチェックを削除する」最適化を行うと、int dead = *P;という（PがNULLだとその時点で止まる）文があることから、if (P == 0) return;に到達する場合はチェックせずともNULLでないことは明らかなので　if (P == 0) return;が消えます。
その後で「使われていない変数を削除する」最適化を行うとint dead = *P;も消えます。

void contains_null_check(int *P) {
　*P = 4;
}

結果、NULLチェックがあったはずのコードからNULLチェックが消えます。何が悪かったかというと最適化の順番……ではなく、int dead = *P;が悪い

例のようなコードそのものを書く人はあまりいないけれど、あれこれやっているうちに事実上これと同じコードになってアというのはありがち

このアカウントは、notestockで公開設定になっていません。

「バグトラッカーなど要らぬ。お前にとって戦う相手とは、自身のイメージに他ならない」

ちゃんとバグと戦って

このアカウントは、notestockで公開設定になっていません。

件、とにかくやりたいからやりたい以上の理由がなさそうな気がしてきた

ニコニコをCoqで証明してみた / Yosh さん - ニコナレ https://niconare.nicovideo.jp/watch/kn3390

このアカウントは、notestockで公開設定になっていません。

DeepSpec/dsss18: Lecture material for DeepSpec Summer School 2018 https://github.com/DeepSpec/dsss18

The Science of Deep Specification https://deepspec.org/main

『定理証明手習い』 – 技術書出版と販売のラムダノート https://www.lambdanote.com/collections/littleprover

このアカウントは、notestockで公開設定になっていません。

Alloy*—A General-Purpose, Higher-Order, Relational Constraint Solver https://aleksandarmilicevic.github.io/hola/

amutake/actario: Verification Framework for Actor Systems on Coq https://github.com/amutake/actario

dschepler/coq-sequent-calculus: Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic https://github.com/dschepler/coq-sequent-calculus

余帰納的(coinductive)な型のsimpl - keigoiの日記 http://d.hatena.ne.jp/keigoi/20100120/1263994563

このアカウントは、notestockで公開設定になっていません。

自宅が死にすぎている、パワがある

ゲーセンでガチャで思い出しましたが、弟がFate/Grand Orderのアーケードゲームをやったといって送ってきた画像を見てやり過ぎだろと思ったのでやり過ぎだろと伝える出来事がありました

このアカウントは、notestockで公開設定になっていません。

cpitclaudel/company-coq: IDE extensions for Proof General's Coq mode https://github.com/cpitclaudel/company-coq

このアカウントは、notestockで公開設定になっていません。

映画を観に行くのえらいっ

Verified Software Toolchain http://vst.cs.princeton.edu/

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

favoriteよりもlikeの方が気軽に言っていい感はある

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

作法の本で、欧州の伝統的な価値観だと公共の場所で靴を脱いで靴下を見せるのはズボンを脱いでパンツを見せるのに近い失礼なので気を付けろみたいな感じのことが書かれていたような記憶がある

あと断りなく他人の足に触れたり靴を脱がしたりするのもかなり失礼らしい

いやまあ断りなく靴を脱がすのは普通に何やってんだなんですが

このアカウントは、notestockで公開設定になっていません。

LPICとLinucの関係調べたのでできる限り中立にメモ https://qiita.com/Alpha_Nine/items/15e4eb478166fcf9008d

「お家騒動で分割するのは別に（どうでも）いいんだけど、さもLPICが廃止されてLinucに移行するかのような報道はやめて欲しいですね。どんだけ金積まれてるかわからんですがEvilすぎやしませんか」それなあっという気持ち

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

スマホ版ことのはアムリラートマジか

TLにもLPICがdeprecatedになると思っていた人いたし本当にア

このアカウントは、notestockで公開設定になっていません。

まあPC版で1周したのでこのままPC版でやりますが

このアカウントは、notestockで公開設定になっていません。

LPI-JapanがLPIと喧嘩別れしたっぽい話はLPI-Japanのプレスリリースにも書かれているので、LinuCにLPIが関わっているという誤解の方はLPI-Japanのミスリードではないですね

LPI-Japan側の言い分だとLPIが自分達の求める質に達していないので縁を切ったみたいな話で、LPI側の言い分だとLPICを持っている人がLPIの役員になれる（LPIC有資格者からLPI役員を選挙できる）ようにするという規則改定にLPI-Japanが消極的だったので日本支部を別に立ち上げたみたいな話

LPICで検索するとLinuCの広告が出てきて笑顔になっています

広告と一番上の検索結果だけ見ると完全にLPIC終わる感を醸し出していて笑顔になっています

このアカウントは、notestockで公開設定になっていません。

MAD CHILD氏の写真初めて見た（名前に反して好青年感ある）

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

気を遣って終わりましたすき

LPICやLinuCが就職に必要な職場に行っても自分に合わなそうなのでつらい

SIer企業にインターンシップに行ったことはあって（というかそこにしか行ってない）、勉強になった

主に、長期間この業界で働くのは自分には難しいという学びを得た

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

ちょうど400 MBですね、4 MBの100倍もある

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

これえらい

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

@beepcap 21世紀なのでMB = 1000^2、MiB = 1024^2で通していきたいところ

このアカウントは、notestockで公開設定になっていません。

SI第9版記念ひとりオフ会をやるぞという気持ちが高まってきた

このアカウントは、notestockで公開設定になっていません。

当方美容院に行ったことがないおたくです

理容室には行くけれど美容室には行ったことがない

フレしゅーのダイマかと思った（？？）

ハングル文字、読む（発音を知る）だけなら非常に簡単（韓国に行ってから調べ始めて翌日にはある程度発音がわかるようになった（韓国語はわからない））

限定SSRが来るはずもないので常に穏やかな気持ちでいる（かなしい）

Certified Programming with Dependent Types http://adam.chlipala.net/cpdt/

"Software Foundations"、しばらく目を離すと新刊が生えてくるのですごい

というかSoftware FoundationsのVolume 4はVerified CかVerified Compilerかなんかだった記憶があるんだけど、いつの間にかVolume 5にVerifed Cが延期されて、Volume 4はProperty-based Checking in Coqになっている

いや、Volume 3にVerifed Compilerが来る予定だったのかな（記憶が曖昧）

Volume 3もVerified Functional Algorithmsになっていますが……

Software Foundationsのコンパイラの巻が出ないの、TAOCPのコンパイラの巻が出ないのに似ている（？）

いつの間にかCoq 8.8に対応した版が出てるしSoftware Foundations本当につよいな

このアカウントは、notestockで公開設定になっていません。

「アイドル筋肉体操」」/「やまぶろ」のイラスト [pixiv] https://www.pixiv.net/member_illust.php?mode=medium&illust_id=70475859

大和さんがずっとにこにこしてるのすき

このアカウントは、notestockで公開設定になっていません。

縦書きで2桁の数を縦中横する場合は1桁は全角で2桁は半角にする

（こともある）

「アルティメット長崎弁」」/「やまぶろ」のイラスト [pixiv] https://www.pixiv.net/member_illust.php?mode=medium&illust_id=70416999

長崎弁レベルが高すぎて厳しい（分かりはする）

アイドルマスターシャイニーカラーズ全然できてないし、月岡さんは長崎出身だなぁという以上の気持ちは特にないけれど、pixivで月岡恋鐘タグのリンクを押しては「月岡さんがそんなこと言うわけないだろ」っつってさめざめと泣いている（泣いていない）

大抵はﾎｰﾝで済むけれど月岡さんだけは月岡さんはそんなこと言わないになってしまう

このアカウントは、notestockで公開設定になっていません。

えらいっ

このアカウントは、notestockで公開設定になっていません。

adminのコメントが端的すぎる

このアカウントは、notestockで公開設定になっていません。

オックスフォード学生気分だ

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

ひどすぎて笑顔になっている

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

Ankalefi lkurftless - Wikirlevip https://wikirlevip.miraheze.org/wiki/Ankalefi_lkurftless

書いた

チェレンコフ光そのものは媒質中でその媒質における光速度よりも速くなんかが動いているというだけなのでチェレンコフ光が見える距離だとどうとかそういう目安に使えるものではないですね

このアカウントは、notestockで公開設定になっていません。

それはそうだろうなあという気がする（長崎にだって「↑長崎」という標識はある）

なんかというか、チェレンコフ放射は電磁相互作用で起きるのでなんでもいいわけではない

このアカウントは、notestockで公開設定になっていません。

偏移ではなく、単に周波数に比例する強度の電磁波が放出されるので人間の目には青く見える（実際は紫外線も出ている）らしい

周波数におよそ比例する強度で電磁波を出すならγ線が無限に出てくるじゃねーかと思うんですがそんなことはないらしい（なんもわからん）

ご飯食べてからことのはアムリラートします（します）

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

Samsung 2nm（Intel 5nm相当）みたいなことは起きそう（？）

EUVプロセスが確立しないと誰もsub-10 nmやらない気さえする今日この頃

このアカウントは、notestockで公開設定になっていません。

nm表記自体は単純で、おおむねトランジスタのゲート（最小）幅のことを指していると考えていいんですが、ある具体的な回路を構成するとどのくらいの面積になるかというのはもちろんゲートの寸法だけでは決まらないですし、会社によってその辺が違うので https://mstdn.maud.io/@omasanori/100632370934137511 のようなことが起きます

まったく同じプロセスでもセルライブラリを変えると面積が変わる

「案内」が通じたとしても案内する先が通じてないと意味がないんだよなあっ #juliamo_learning_battle

入浴シーンがあるからことのはアムリラートは共有スペースでできないんだよなぁ #juliamo_learning_battle

カタカナで表すならイマージですかね

ありがとう ne、niv xaceじゃん（？） #juliamo_learning_battle

ノベルゲーム経験がないので攻略のセオリーがわからない #juliamo_learning_battle

とりあえずマッピングよろしく選択肢を記録していくか #juliamo_learning_battle

最初の内にごめんなさいとありがとうを学ぶの偉いよ #juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

まだ問題を解決していないループもの主人公だ

ルカが実はヤバいことがわかる2周目（1周目からヤバかった気もする） #juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

（ボスッ） #juliamo_learning_battle

（凛のお腹に抱きつく音）が打撃音に聞こえる不具合 #juliamo_learning_battle

唐突な数詞講座
#juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

激強マシンだ

このアカウントは、notestockで公開設定になっていません。

フォローインポート、送ったらすぐに全部やるんじゃなくてキューに入れてゆっくりやるというのは問題を緩和しないのでしょうか（FSWのアーキテクチャよくわかってない）

タ　イ　ト　ル　回　収 #juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

確かに、急激には変化しないだけで最終的なトラフィックは同じですね

お　　　ま　　　た　　　せ
ことのはリーベツィーウング
　い　 　つ　 　も　 　の
#juliamo_learning_battle

ユリアーモはみんなの「ことのは」 #juliamo_learning_battle

文字の名前と単語としての発音 #juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

もうちょっとビルドの負荷が低い言語ならもっと容易だけどRustだと厳しい

凛 death #juliamo_learning_battle

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

名前を書かれると支配される呪術的な話かな？（？？） #juliamo_learning_battle

Twitterでの知人を探すには http://bridge.joinmastodon.org/ が使えたり使えなかったりします

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

茜ちゃんは茜ちゃんでも葵ちゃんの声がする茜ちゃんってなーんだ？

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

鯖缶の好きなものは？に「人類」とか「平和」とか送りまくって「おかしい……なぜ通らないんだ……？ 」しような

メッセージをより効率よく配送する仕組みなぁ

あひるさんが信頼を失ったのが見えた

このアカウントは、notestockで公開設定になっていません。

メリットがなさすぎる

ディケイドも10年前なんだよな

ジオウ1話見損ねました……

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

えらいっ

このアカウントは、notestockで公開設定になっていません。

モンスターハンターワールドなぁ

これすき

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。