なんか Prolog がやること、形式操作で自動証明をするのを手動で紙とペンでやる演習を講義でやらされまくった

このまえの情報処理学会 プログラミング研究会の五十嵐研究室（京大）からの招待講演、RustHorn っていうホーン節な論理学と「預言」の概念で Rust に形式証明つけるお話だったのを思い出した https://x.com/shiatsumat/status/1798335251015684340

Prolog はホーン節に標準化した一階述語論理を解くソルバなので

人類の人類に対する倫理

ある年の GW で新生～蒼天をサブクエスト込みで一気に終わらせたけどあまりに人生をもってかれすぎて恐ろしくなって封印してから２年くらい経ってる

まだ紅蓮入った直後ですいませんになってる

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

FF14 だいぶ止めてたけど再開してもいい気持ちになりつつある

他開症

JavaScript V8 エンジンに匹敵する異様に高速な処理系を誇る LuaJIT、なぜかそれを個人で成し遂げてる未来からきたコンパイラ作成ロボットみたいな Mike Pall のクローンをつくるのが issue に上げられてるのまじでいいな

Clone Mike Pall · Issue #45 · LuaJIT/LuaJIT · GitHub
https://github.com/LuaJIT/LuaJIT/issues/45

ぷよぷよeスポーツ | SEGA
https://puyo.sega.jp/PuyoPuyo_eSports/

【公式】ぷよぷよeスポーツ×プログラミング
https://puyo.sega.jp/program_2020/

@prime へーしゃたぶんいろんな仕事あるよ

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

広告強奪店

“Plan 9から派生したInfernoでは tar(1) コマンドが無くなっていて、代わりにgettar(1)で置き換えられている。他にも puttar(1) と lstar(1) があって、それぞれ tar x, tar c, tar t に相当”

Plan 9とInfernoにおけるtar(1)の変化 - Plan 9とGo言語のブログ
https://blog.lufia.org/entry/2024/06/27/212803

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

この経緯からか、東芝ブランドの TV である REGZA がガルクラ推しで、なぜだか川崎のビックカメラも川崎のヨドバシカメラもずっと REGZA の展示品で一生ガルクラをループ再生してる

@akahana それあかはなさんの脳内だけだよ

『ガールズバンドクライ』は舞台がそうというだけでなく川崎市や川崎市に所在する企業がエンディングクレジットにまで掲載されてタイアップしている。
ちなみに、川崎駅の目の前のところは東京電気株式会社が昔存在していた。今の東芝である。（そんな昔から東京じゃないのに東京って……）

追記した。最終的に、ほぼ OS の概念そのものの起源に近い Fernando J. Corbató 教授の Compatible Time-Sharing System (1961) に Stelltzer 教授が 1964 年に追加した ARCHIV コマンドにまで遡れそう

blogged >> 続・tar(1) はなぜオプション引数にハイフンが不要なのか？―tarとkey argumentsの起源を更に辿る https://orumin.blogspot.com/2024/06/tar1-tarkey-arguments.html