In einem Thread darüber, welche Programmiersprache man lernen sollte, sah ich, dass jemand Lean4 und Haskell erwähnte. Persönlich glaube ich, dass man Lean4 nicht in Betracht ziehen muss, es sei denn, man studiert Mathematik. Lean4 kann zwar als allgemeine Programmiersprache betrachtet werden, aber das gesamte Code-Management und die Nutzung sind nicht ganz zufriedenstellend. Als formale Verifizierung für mathematische Beweise (Beweisassistent) ist es jedoch ausreichend. Im Vergleich dazu ist Haskell zum Verständnis der funktionalen Programmierung oder der Implementierung mathematischer Beweise in Programmen besser geeignet, obwohl es ebenfalls sehr experimentell ist. Außerdem gibt es Racket (moderneres Lisp), das auch sehr praktisch und lehrreich für die Erforschung der funktionalen Programmierung ist.

TLDR For just 60 RMB, get an RP2350 development board, flash it with the PicoKey firmware, and you can create your own open-source hardware security key to use as a budget YubiKey. It supports FIDO2 login and OpenPGP, but the hardware login and encryption functions cannot be used simultaneously. The steps are simple: buy the board → download the firmware → hold the BOOT button while plugging it into your computer to flash the firmware → initialize via the web config page → done. Perfect for cheapskates (like me) who don’t want to spend hundreds on a YubiKey but still want to play with hardware keys.

【AI Summary】Under state-owned-enterprise secrecy rules, the author hand-rolled a CLI password manager, RPaWoMaster, in Rust—balancing relative security with convenience, and documented the full journey from Python to a standalone binary.

I’ve got a handful of domains, but only two I really use. For ages I piggy-backed on Yandex, yet “nice but paid” plus random bursts of Cyrillic finally wore me down. After years of this dance, I finally snapped: let’s run our own mail server.

小杂感¹

蜜蜂的刺，一用即丧失了它自己的生命；犬儒²的刺，一用则苟延了他自己的生命。

他们就是如此不同。

约翰穆勒³说：专制使人们变成冷嘲。而他竟不知道共和使人们变成沉默。

要上战场，莫如做军医；要革命，莫如走后方；要杀人，莫如做刽子手。

既英雄，又稳当。

与名流学者谈，对于他之所讲，当装作偶有不懂之处。太不懂被看轻，太懂了被厌恶。偶有不懂之处，彼此最为合宜。

世间大抵只知道指挥刀所以指挥武士，而不想到也可以指挥文人。

又是演讲录，又是演讲录⁴。

但可惜，都没有讲明他何以和先前大为两样了；也没有讲明他演讲时，自己是否真相信自己的话。

阔的聪明人种种譬如昨日死⁵，不阔的傻子种种实在昨日死。

曾经阔气的要复古，正在阔气的要保持现状，未曾阔气的要革新。大抵如是，大抵！

他们之所谓复古，是回到他们所记得的若干年前，并非虞夏商周。

女人的天性中有母性，有女儿性；无妻性。妻性是逼成的，只是母性和女儿性的混合。

防被欺。

自称盗贼的无须防，得其反倒是好人；自称正人君子的必须防，得其反则是盗贼。

楼下一个男人病得要死，那间壁的一家唱着留声机；对面是弄孩子。楼上有两人狂笑；还有打牌声。河中的船上有女人哭着她死去的母亲。

人类的悲欢并不相通，我只觉得他们吵闹。

每一个破衣服人走过，叭儿狗就叫起来，其实并非都是狗主人的意旨或使嗾。叭儿狗往往比它的主人更严厉。

恐怕有一天总要不准穿破布衫，否则便是共产党。

革命，反革命，不革命。革命的被杀于反革命的。反革命的被杀于革命的。不革命的或当作革命的而被杀于反革命的，或当作反革命的而被杀于革命的，或并不当作什么而被杀于革命的或反革命的。

革命，革革命，革革革命，革革……。

人感到寂寞时，会创作；一感到干净时，即无创作，他已经一无所爱。

创作总根于爱。杨朱无书。创作虽说抒写自己的心，但总愿意有人看。

创作是有社会性的。但有时只要有一个人看便满足：好友，爱人。

人往往憎和尚，憎尼姑，憎回教徒，憎耶教徒，而不憎道士。

懂得此理者，懂得中国大半。

要自杀的人，也会怕大海的汪洋，怕夏天死尸的易烂。但遇到澄静的清池，凉爽的秋夜，他往往也自杀了。

凡为当局所“诛”者，皆有“罪”。

刘邦除秦苛暴，“与父老约，法三章耳。”而后来仍有族诛，仍禁挟书，还是秦法⁶。法三章者，话一句耳。

一见短袖子，立刻想到白臂膊，立刻想到全裸体，立刻想到生殖器，立刻想到性交，立刻想到杂交，立刻想到私生子。

中国人的想像惟在这一层能够如此跃进。

九月二十四日

【注释】