在一个学什么编程语言的帖子中，看到有人提到了Lean4和Haskell，其实我个人感觉，除非是数学类专业，否则就不用先考虑Lean4了。 Lean4的确可以作为一般的编程语言来看，但整体代码管理、使用都有点不那么让人满意。 但作为数学证明的形式化验证（辅助证明器），这些就足够了。相比而言，为了了解函数式编程， 或者数学证明在程序中的实现，Haskell可能更适合，虽然其实验性也很强。 另外还有Racket（更现代的Lisp），在函数式编程的探索上，也很有实践和学习的意义。

TLDR 花60块买个RP2350开发板，刷入PicoKey固件，就能自制开源硬件密钥，当便宜版YubiKey用，支持FIDO2登录和OpenPGP，但硬件登录和加密功能不能同时用。详细步骤：买板子→下载固件→按住BOOT键插电脑刷固件→网页初始化配置→搞定。适合不想花几百块买YubiKey又想玩硬件密钥的穷鬼（比如我）。

【AI Summary】在央企保密要求下，用 Rust 手搓了一个 CLI 密码管理器 RPaWoMaster，兼顾相对安全与便捷，并记录了从 Python 到可执行文件的全过程。

【TL;DR】放弃 Yandex，改用 poste.io 自建邮箱，踩坑 DNS、rDNS、反代，虽不完美却乐在其中。

小杂感¹

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

他们就是如此不同。

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

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

既英雄，又稳当。