关于

关于我

这里是 Yurin,你最近过得怎么样喵

之前的 Zine 姑且算是弃用了,Zine 天天 break change 实在是没有现代性

说不定可以写出什么有意思的文章说是,但其实这种可能性非常渺茫,毕竟我只是个普通的复读机

喜欢 IBM Plex 所以本站 all in Plex Sans (Mono 也是极好的)

这可能会造成一些流量费用,但为了字体排版,我觉得这非常值得

But However Whatsoever

反正并不会比你手机里那些奇奇怪怪的国产应用的热更新包更大,甚至可能还没一个开屏广告占的空间多

可能会搬一些之前在 Hexo 上的东西来,如果有时间的话(也就是大概率没时间)

全志 allloser 的工具链怎么那么难用 (虽然名字叫 Allwinner,但总觉得在环境配置上我就已经 all lose 了)

瑞芯微的 SDK 怎么 50 GiB 啊 (甚至还不包括编译出来的产物,我的硬盘在悲鸣)

为什么嵌入式开发的文档总是像在读各种毛选第五卷,而且还是那种残缺不全的

如果什么时候能在这些邪道国产 SoC 上跑起来主线 Buildroot,那我大概也就圆满了

说不定也会搬一些其他东西上来,虽然估计没有人乐意看

wasi 是怎么做到每况日下的?

是不是现在流行发一些奇奇怪怪的量表结果?

那 INTP 5w4 5-4-1 // 我宣布这是消费主义的胜利了,顺便把我也定义成了某种可以被贴标签的商品

怎么大家都去搞大模型了?

希望本站内容对您有所帮助,或者至少能让你觉得“这家伙居然在用 SvelteKit”

Stay healthy and be well.


目前可以公开的情报

是银河系土著

不是为了卖玩具/小人/棋子/规则书诞生的

距离神圣泰拉不算很远,大约 0.000000000021 万光年,在物理层面上还没被大裂隙切开

是人亚族的成员,碳基生命,主要通过摄入咖啡因和二次元内容维持生物电信号

目前尚未表现出任何觉醒亚空间灵能的迹象,但这并不妨碍我在编译失败时试图通过意念修复代码

如果你在猎户座旋臂附近找不到我,那我可能正在摸鱼

不讨厌十三世纪前的维京蛮子,只要他们不到我家来

一般不会参与吉哈德/十字军东征/再征服/三十年战争

也不参与大远征,因为我真的很怀疑那几个掉进亚空间的基因原体是被代码 Bug 带跑的

遵守《星际迷航》的第一指导原则,即绝不干涉低级文明的自然进化过程,除非他们试图用 Word 来写代码

五维大概都不能进行超过 (-2, +2) 的难度修正

在长休时只能准备一个二环法术

尚未植入任何赛博义体

QA 环节

你为什么要写这个网站?

因为我看别人都写了。

你的文章是给谁看的?真的有人会看完那些数学公式吗?

给 KaTeX 渲染器看的。只要它没报错,我就默认已经有人完整读完了。

卫生宏能阻止你的代码腐烂吗?

排水系统不能完全解决城市卫生问题,不代表跳大神可以防疫。

既然全性不可判定,你怎么知道你的博客构建脚本会终止?

但是在 StepStep 内图灵机是可以判定的,如果我等不及了,我会在旁边按 ^C

写了这么多关于类型系统和形式化的文章,你的项目里有用 Coq 或 Agda 证明过正确性吗?

正确性往往是靠 test case 和不断涌现的 CVE 保证的,我尽量不尝试去证明它们的正确性,不然可能会毁掉这些优美的证明语言。

SvelteKit 5 出来的时候你会再重构一次吗?还是说你已经接受了技术债务是人生常态?

个人博客的第一生产力从来不是写文章,而是重写博客本身。只要我每隔两年换一套静态生成器从头重写,旧的技术债务就会在物理意义上清零。

你真的理解 monad 吗?还是只是会用那句'endofunctor category'的梗?

我不是一个可观察对象,所以需要知道我的了解程度的话,你需要一个 Comprehensive<T where Human> Monad 来观察我。

如果代数效应这么好,为什么主流语言都不用?是他们错了还是你错了?

主流语言当然在用,只是他们更喜欢每隔十年把代数效应拆成一个个残血的语法糖(比如 try/catch、yield、async/await),当成全新特性再卖给程序员一次。

IBM Plex 能拯救你的排版,但谁来拯救你的 Git commit message?

给别人提交

bash
$ git commit -m "fix(semantics): fix the unchecked type variable after coherence step so lower bound can be inferred."

自己写

bash
$ git commit -m "111111" #只是在触发 CI
你对停机问题的理解,是来自教科书还是来自盯着 webpack 看了三个小时?

我入行晚,所以停机问题的理解来自盯着 cargo build 看了三个小时。

Zig 真的会取代 C 吗?还是说你五年后还在写 Makefile?

最现实的演化路径是:五年后我依然在全志和瑞芯微的祖传 SDK 里对着三十年前的 Makefile 磕头,但偷偷把编译器换成了 zig cc。

良基归纳能证明递归终止,但能证明你的项目不会烂尾吗?

恰恰相反,它证明了我的项目必然烂尾——既然人类的三分钟热度是严格单调递减且有下界的,根据良基归纳,我的所有项目都会在有限步内收敛到“弃坑”这个 Base Case。

你在文章里批判 C 预处理器的文本替换,但你的博客构建流程不也是一堆 Node.js 脚本拼起来的吗?

请尊重现代前端工程化:我们操作的是 AST,这叫“结构化屎山”,和 C 预处理器那种“纯文本屎山”在代数结构上有着本质的区别。

Rust 的 borrow checker 拒绝了你多少次?

零次。信贷是资本主义的幻觉。

如果你这么喜欢类型安全,为什么还在用 TypeScript 而不是 Haskell?

因为浏览器还没学会在 DOM 里直接跑 GHC;而且偶尔在代码里偷偷写一个 as any 带来的背德感,是纯粹的函数式语言给不了的。

你的博客用 SvelteKit,但你的个人项目有几个真的部署上线了?

我的 FDE capability 只含 Svelte。

对角化论证能证明停机问题不可判定,但能证明你不是在拖延正事吗?

不需要证明,因为“在博客里回答这个问题来论证自己没有拖延”本身,就已经在对角线上构造出了一个新的拖延行为。

自由单子真的 free 吗?还是说你付出的代价是向每个朋友解释什么是 monad?
is_free?MonadAirFriendCommoditiesvoid* ptr
in theory#t#t#t#f#t
in RAM#f#t#t#f#f
in reality#f#t#f#f#f
as in sugar-free#f#f#t#f#f
你写的这些技术文章,是为了分享知识,还是为了说服自己真的懂了?

高成本的小黄鸭调试法,唯一的区别是小黄鸭不会顺着网线过来指出我第三段推导写错了。

LevelDB 的 LSM-tree 很优雅,但你上次手写 B-tree 是什么时候?

分子生物学家研究发现,LSM-tree 实际上是很像树的链表,而不是形似链表的树。和 B-tree 相似是因为相近的生态位造成的趋同演化。

你批评 WASI 每况日下,但你为此做过什么贡献吗?还是只是在博客里抱怨?

我为 WASI 做过最大的贡献就是不断地抱怨它每况日下。 正如 B.Stroustrup 所说

世界上只有两种编程语言:一种是经常被人吐槽的,另一种是没人用的。

我正在帮助 WASI 逃离第二种。

有趣的项目

  • snake guide 试图通过写贪吃蛇来骗纯洁的学弟学妹们入坑 C 语言
  • EasyScan 解决“怎么又没签上到”这一生存危机的科技化救赎
  • LDTI 将拉康心理学和庸俗心理学完美结合,并不试图解决你的心理空虚
  • Zig Chip-8 用 Zig 写的模拟器,运行它的瞬间你会觉得自己正在和 1970 年代的 CPU 灵魂共鸣
  • yacrawler 一个除了爬虫本体什么都没配的极简框架,主打一个“不仅能用,还能让你自己动手补代码”的锻炼机会
  • Zig Cbor 在二进制的海洋里反复横跳,只为解析那该死的 CBOR

膜拜的大佬们

  • 依云 Archlinuxcn 的守护神,如果你在群里看到有人发“/help”,那通常不是在求助而是在召唤她
  • Andrew Kelley 也就一做游戏的,他懂个锤子系统编程
  • Lina Hoshino 百合真好吃.jpg
  • Bellard 不要凝视古神,因为古神正在忙着把整个 PC 模拟器塞进 JavaScript 文件里

友情链接

  • Angine04 无所不能的前队长大人
  • moe 被图形学耽误的特异人士,魔法使(物理)
  • 洛菱 游荡在各个次元的神秘学长
  • 碳酸氢盐 资深 Key 厨,大概在寻找光玉