本质上也不难理解，lo 就如同文件系统上的文件，对其操作必须「独占」该资源的控制权。在 pg 上恰好可以依赖事务机制保证操作的原子性

#learn #life #dev #pl #cs 这周的笔记 📓

有些和某些东西有关的我会转发到 Throws，至于图什么的待会发，因为照片转发到电脑上有点不方便...

+ 悲观的 2018 与形式化证明

2019 可能会是过去 10 年里最差的一年，但却是未来 10 年里最好的一年。

如何形式化地论证这个命题成立呢？

因为我现在太菜了，不是很熟练 Agda 的形式化证明，所以这可以说是 #TODO （
对不起啊，而且我也怕这花费太多时间

当然，上面我说过的那个东西后来发现其实有错误，我误会了，比如

(有火 -> 有烟) 这个复合命题是说『如果有火，那就有烟』
假设这是既成条件（它已经成立）。
但是我上面的表达是：

(有火 -> 有烟) -> 有火 -> 有虫也

其实我的目的是表示已经证明上面那个有火就有烟成立之后，由

有火 

推出

 有虫也

这是不对的，因为 (有火 -> 有烟) 是既成条件，它已经成立了，而上面那个命题实际上是说『如果』一个既成条件已经成立，这是废话。
当然这么说在上面那个文字里面没错误，但是容易引起误会

当然这些都是很 trivial 的东西，我现在正在为如何独立理解冰封博文教的归纳证明 \forall{xs}.\quad reverse \quad (reverse \quad xs) \equiv{xs} 头晕呢
其实如果不是有这篇博文，我对递归的理解不会有再次的加深，为了理解此归纳证明我以不同的可视化方式对 rev 1 :: 2 :: 3 :: [] 和它相关的东西不断弄了十几次，最后还是没能理解
当然第二天（今天）算是勉强理解了一点，但我还是无法独立证明...

+ 我妈水问题和 #PL 理论的表象类型

我妈水问题... 都知道？

女朋友对你说：我和你妈同时掉到水里，你救谁？

演讲者的意见就是这类问题不涉及实际场景是没有太大讨论意义的

我懒得把他的话再复制一遍，不过这个问题很像你们平时讨论的 C++ 和 #Java 哪个好、MySQL/Percona/MariaDB 和 PG 哪个好，GNU/Linux 和 Windows 哪个好、Vim 和 Emacs 哪个好（虽然很多人连 C-x C-b 在 Emacs 里是干啥的快捷键都不知道）

其实我的意思很明确也相当迫真，就是说，我们抽象讨论的时候就是编译器处理程序的阶段，实际处理问题的时候就是程序实际执行的时候

有些信息只有到了『运行期（runtime）』才会知道，比如一个 Java 这种经典 OOP 里参数实际的类型，而不是简单一个可以被继承，可能有 subtype （子类型）的非 final 类

所以 JIT 编译可以做一些 AOT 做不了的优化，就比如说数组访问边界检查消除，比如说分支概率预测，比如说一些运行期可以确定信息而不是常量的剪枝
（当然 AOT 也是有自己的好处的，不是 JRockit 这种面向服务器的 JVM 一般都要专门设置 server compiler JIT 编译器才敢多弄点优化措施）

相关的博文 R 大的博客上是有的，推荐阅读。不学习就会死啊！每次想着这个，learn or die 啊，说不定你就愿意学了（当然前提是你要尝试让自己相信，不学就会死，然后或许你会学（

当然，时间的朋友这演讲我觉得讲得还不错。对于一些『做实事』的人都是很有价值的。我觉得值得一看。当然是收费的（其实只是要优酷 VIP），但有价值的东西是值得你为之付费的。
如果你是 Geek 之类有些人会对这种不良心平台『恨之入骨』的，也算了，不过我觉得不是原则性问题一般都能容忍，换句话说，现在也没人能替代优酷，是不？上次知乎 #ZhiHu 的 #China #LGBT 水晶之夜（当然其实本质上是政治正确，不过它太自觉了）

就像是现在过气的新蛤社的 GoliGoli，和以前的 GeekApk，说到 #GeekApk... 绿色... 猴子... 文体两... 多多支持... 停下停下停下 🙃，当然 GeekApk 可能不会复活但我自己这个寒假（20 多天）可能独自会再起一个同样性质的项目，我不作任何担保说绝对会完成，但我相信基于我目前的表现你们会信我有完成它的技术资本。或许如果真的做出来了你们会用？（

就像曾经 @drakeet 吐槽的那样，其实 GeekApk 最大的问题在于过于功利，不像是在做事，而是很多没经验的人在瞎搅合，而真正为它写过一两行真正意义上有用代码的可能只有我和 @zhy0919(losfair) 两个人，当然我自己很冤，因为我本来不是功利的。我开始的计划虽然很幼稚，不像『做事的人』，但起码我也是细化了我的设计的，而且我从来没有计划在它完成之前就拿出去吹，或者找别人一起帮忙开发，我不指望有人能为不是自己的工程做啥贡献。自己的东西有人用都是万岁了。

虽然我那时的确是没有独立走到实现阶段的能力，但我也不只是会弱智地坐在那里想着『创建一个 Geek 社区』而无所行动，起码我是写了东西的，所以我觉得这事，谁开始『幼稚』的时候都会有的，我不后悔。

没有一个一个 '1' 积累起来也达不到 '10'，谁都不是空中楼阁。即使是天才也曾经有啥都看不懂的时候。所谓人的经历是有连续性的，不会有现在的天才是『突然开窍』而自己完全没有相关背景的说法

+ 知识的深度和广度

深度优先搜索和广度优先搜索大家都知道吧（当然我不是说这个
不过我不知道现在 #OI 生是不是所有人都会这种简单问题的，据说也有人不会？

当然现在软件工程入门门槛太低了，能模式识别，抄改代码都可以开发很优秀的 Android 应用了... 算法什么的不是必会的，你们就需要知道 Regexp.new("[\u4e00-\u9fff]*").match("字").size 可以拿来统计汉字字数，不需要知道后面 Unicode、Regex 引擎理论之类的（当然这个不是最佳实践，如果要开发实际应用的话 #Unicode 还是有些东西必须处理的，不然字数统计有问题）

所谓深度大概就是从小白（只会玩个游戏）、到用户（基本啥都不懂）、到 Geek（可能有看代码的能力）、到幼稚的开发者（抄改代码）、到普通开发者（至少会自己写复杂一点的代码了）、到企业级的开发者（有一定经验了）、到开发者依赖的开发者（知道自己真正在干什么）、到程序大师

再比如说，一个 #JavaScript 开发者可能在他自己的领域，比如 Xml/Js/AsyncIO 可能有所了解，但如果要去弄逆向工程或者 CTF 这种要求知识面和深度都有的东西，可能就啥都做不了了，他们眼里『二进制文件』和『二进制文件』... 根本没有区别嘛，而相当多一部分包括 ES6 的 JavaScript 开发者可能都没有用过 ES6 新的 ArrayBuffer

而一般来说，C/C++ 开发者的素质都比 JavaScript 开发者的素质高，我们可以认为主要写 JavaScript 的人往往比较难学会写 C/C++/C#，而写 C/C++ 之类的人全都有能力去写 JavaScript，这里我们可以看出一个深度的区别，虽然本质上还是知识面的，但从一些常见的例子看可以理解为是深度一样的东西

也就是说，深度就是从简单顺序结构到循环到递归的差别，广度大概就是同一个层次的东西了解很多，我懒得弄什么形式化定义，你们看懂就好。

最简明的代码例子（ #Kotlin ），当然因为我也很小白所以没有特别酷的例子可以弄，但我至少也不至于像王淫那样拿非常简单的 #FP 例程去骗你们说是他觉得最优雅的代码，我到觉得是他在嘲讽你们，这都看不懂 ：）
我当时就看不懂，我相信你们很多人（不是写 Scala、Clojure、Eta 的）也看不懂。

假如我们写个最简单的 FizzBuzz 程序

== 这是普通小白会写的代码，当然其实有隐含的事实，就是他们的代码是抄来的（控制结构），自己连 .. 是什么都不知道，可能

fun main(args: Array<String>) {
  for (i in 1..100) {
    if (i % 3 == 0 && i % 5 == 0)
      println(i)
  }
}

== 这是稍微有点常识的普通人（上文的『企业级开发者』）会写的代码

fun main(vararg args: String) {
  for (i in 1..100)
    if (i % 15 == 0) println(i)
}

也可能是

fun main(vararg args: String) {
  (1..100).forEach {
    x -> if (i % 15 == 0) println(i)
  }
}

之类的，看他们的觉悟了，其实这就是属于已经开始理解对算法的表述方法还有程序结构的类型了，至少他们不止了解一些『常用』的方法

== 这是又有点常识的人会写的代码

fun main(vararg args: String) = (1..100).filter { x -> x % 15 == 0 }.forEach(::println)

当然我这么说也有点迫真，其实这个例子举得不好，举例子向来都是最考验一个人技术的。

我技术不好。不过如果要举一个更好的例子，我猜是算法题。

+ 关于 @ohcnzz 人肉李先生（李宗阳）的一些看法 #statement #China #sb （撕逼）

（当然现在某羊分享机场场主也已经承认自己是李先生了，所以这里就称他为李先生

Oh CN ZZ （就是 Telegram 版恶俗维基）这个频道的一些背后的维护者、组织者... 怎么我突然有点感觉好像里面一些人好像我还认识怎么的...

如果真的是有这样的朋友在此频道里，建议以后对像李先生

我感觉 Oh CN ZZ 现在维护起来都有点像是为了搞笑（我想，在信息安全上，随便侵犯别人隐私，随便控制别人的东西一定很兴奋，因为我也这么干过，那可真的不是一般的爽）而维护

我想它大概就是创立来泻一些人公愤的频道，但说实话，虽然李先生的确很傻逼（真的）

我觉得，就比如这次的例子，李先生是在自己的免费机场（就是科学上网的梯子）声称要打所有收费机场
想必诸如 CloudHammer 这种梯子的维护团队肯定很生气，而且远远不止这一家，所以员工们就组织起来去举着『正义』的旗帜『侵犯』李宗阳先生
但这的确是侵犯，而李先生，我觉得其实为这点事（说了句气话，但他还的确没有去打什么商业机场，只是自己独自意淫商业机场被打的情况而已）而不断挑拨他，然后维持 @OhCNZZ 更新的这种行为

最后甚至把人家身份证、百度网盘、家庭电话号码等非常隐私的东西都公开，以至于使用此机场的吃瓜群众都难以幸免被碰库（当然手段不一定是碰库，反正这里就是指尝试得到用户设置的原始明文密码这种行为）

着实不是多么令人称道（暴论）

这条消息我知道由于 Oh CN ZZ 的特殊性，内部人员肯定是不应该回复的，或许我也有误解，不过如果我的确是误会了，而李先生就是可憎的，他所受的一切就是应得的，就请大家谅解。

为小鬼说句公道话，如果以后再有类似的小鬼，我想大家都看到的时候，可以稍微忍受一下，受不了了再去弄他们也不为过（当然是要类似天安门事件的『蕞大限度的容忍』，比如迫真 DDoS 而非 DoS），但自己没有实质性的损失就去弄这种小鬼着实不好

+ 篮球很菜的

隔壁 LWL 称我『会这会那』好厉害啊（其实首先就是还没到样样通，另外的确是样样松
我真的不会打篮球... 正在学，不过我觉得学习效果还不错，别人都是打了几年的，而最近一次仅仅一两个小时我就从只能看着篮球到能够比较弱的背后传球了，并且学会了通过感知和粗略估计球体离地高度曲线和频率什么的来『救死球』，虽然那花了很久....

而之前我爸逼着我学的，是除了投篮之外啥都不会，可以说（三步上篮都没有学会

+ LWL 好大佬啊（顺路科普急救

LWL 真的好厉害啊 #life

今年做了不少社会实际活动呢，很羡慕的说

CPR （心肺复苏）的话，一些比较紧急的 case，比如身边的人心脏病突发，心脏骤停

是非常危险的，在求助、120 电话之余，若不能在 3 分钟内看到急救人员，或者无法确定时间

这时就必须实施 CPR，因为已经非常危急了，再过两分钟可能就凉了，或者就是脑死亡植物人。
这时候我觉得道德上可以说是绝对没有问题的，因为你做了别人可能就活，或者至少是最后可能醒，不做就是一个死，这种情况都是比较无奈的，那我觉得即使因为做了出现什么意外情况导致情况恶化（e.g. 实际上人家是伴随内出血，而按压加重了内出血）的，也不能说是有责任。

流程很简单

CPR involves chest compressions for adults between 5 cm (2.0 in) and 6 cm (2.4 in) deep and at a rate of at least 100 to 120 per minute

按压深度大家能自己感受到就可以了。频率是每分钟 100-120 下，就记 100 下是不会错的。
30 次按压需要辅助 2 下人工呼吸，就记大概 15 下一次也行，一个大概的频率

我相信大家虽然不是非常了解我们人类身体一些非常内部的条件机制，但至于平时容易出现的突发情况，还有一些『病症』和『解释』是做得到的（比如出车祸是什么情况，别人突然昏倒是可能什么情况），这是生物基本，小时候看过《十万个为什么》大概都知道。

+ 图解 XXX

本来 duangsuse 是想举个例子推荐大家使用图解的方式来学习，而且对我个人来说，基于这些图示分析的确是相当有效率
但 duangsuse 考虑到自己时间有限，就不教大家画了（

+ 为何我不能创作音乐？

我不是真正完全不能创作音乐，就目前而言，效率比一年前高很多很多，比较不用考虑灵感的问题（非常随性的话，不是命题作文），只不过全都是内建的... 我自己对编曲是完全没有学

其实一些简单的 Pattern，还有组合他们，我都是完全会的，不过有些东西还要经验和更好的选择能力，我以后可以考虑一下再去总结一些规律什么的...

最大的问题其实在于如何记录灵感。我对时值实在是不怎么敏感，而且我音高也达不到可以直接映射到 C4 C5 C#4 D#1 这样的水平，所以我可以说除了自己唱或者能即时能听觉反馈之外无法保持这些 pattern，没有 pattern，没有曲子...

目前还在解决这种问题，我不着急。

+ 绘画：原地打转 or 向前再出发

duangsuse 开始画一些简单的画了，主要还是铅笔的未上色 lineart 为主，水粉之类我有了数位板可以再考虑。

以前，变化是生活的一部分；现在，变化成了生活本身。——和菜头

环境在变化，时代在进步，不随着它向前，等于你落后
然而因为自己跟不上大环境而咒骂大环境为什么不止步不前的人，也太过分了吧

对于现在的软件开发者来说，要么然就像一些计算机科学爱好者一样向下钻，学会那最朴素而守恒不变的真知而后能『知其变，守其恒』，要不然就乖乖跟着时代向前走，不要老想着『学』猝死学猝死，猝死不是学习的罪，是不会安排时间的过失。

我觉得很奇怪，为什么一些工程师终日都不愿意稍微学习一下，好像一次学习就管终身了一样，产业界的一些工程师都说即便是他们一两年也会遇到一个尴尬的情况：技能纯熟了，没有挑战了

以至于自己的技术数十年如一日还是那个熊样，或者完全没有踏出自己的『领域』半步，该是前端还是前端，该是设计还是设计

自己在自满于那点『相当了解』『十分清楚』的技能树（这是 LWL 的说法，我觉得技能栈还是技能树其实都差不多，板凳条凳问题，无可厚非）时，是否有看到于自己同道的人，已经走出了『看不到自己看不到的东西有多少』的阶段，开始写各种教程甚至出书，以至于开始创建一些崭新的东西呢？而此刻，自己还在打游戏？

我觉得喜欢的东西是打游戏其实没什么，认清自己，有最起码的自知之明就是好人。虽然不是优秀的工程师，但称职的工程师也是极好的。任何看不清自己的情况，一般都会被别人引喻为无知甚至幼稚。

比如某些在 node 的 TypeScript 版继任者（可以这么说） ry/deno 那里叫板不要再更新了再学要猝死了，其实他们都知道 deno 和 node 到底是干什么的吗？还是只是把它作为一个通用的运行环境，不知道 Node 这个『Async』是什么意思，或者是只知 Async，哪怕是很简单的一些协程、并发就不会了呢？

宏观是我们必须接受的，微观才是我们可以有所作为的。——查理·芒格

遇事找客观，越找越悲观，遇事找主观，越找越乐观

客观的大环境你是没法改变的，但是你可以找你自己可以做的事情，然后去解决自己的问题，不要在无用的地方空转太多时间。

自己技术不过关以至于无法跟上时代的步伐，反而咒骂时代走得太快，我不知道这是自己的错还是时代的过失。

凡我赶不上的，我就做好准备，到未来等它。

#Telegram 这个设计比较好玩，就是如果是被别人转发的链接，即使自己被 BLOCK!!!! 了还能看？？？

#sysadmin #linux #arch #archlinux 我觉得嘛，其实 Arch Linux 还是不是特别的需要用户的系统部署管理水准的，一般人在普通 x86_64 PC 上都会比较好弄，除非是配置特殊要专门驱动的话，Gentoo 会稍微难一点，emerge 相比 pacman 概念也更复杂（当然 Gentoo 的包管理系统是叫 Portage，其实也可以说约等于 pacman + AUR，用起来稍微复杂一些），Arch 其实很友好了，建议试试。BlackArch 的话我觉得不如 Kail 好，所以还是推荐 Kali，不过 Arch 要加 BlackArch 的包们其实也可以的，但是，有时候工具的数目，开箱即用并没有那么重要

似乎 我现在格盘装 Kali 可能折腾量还少一点…或者很多
不知道是换发行版框架所带来的学习成本太高还是 Arch 本身带着一股「生人勿近」的气场

再见，我用 Kali 去了（

#dev #tech #English

boot 靴子 引导
stub 存根 占位
review 复习 评审
render 提出 渲染
map 地图 映射
console 安慰 控制台
frame 边框 帧
image 图像 镜像
bus 公交车 总线
access 入口 访问
log 伐木 日志
dump 倾倒 转储
cache 隐藏住所 缓存
port 港口 端口
performance 演出 性能— adolli🍮7️⃣🎏咕嚕靈波（●´∀｀）ノ♡ (@adolli) January 3, 2019

最终没能完成的 #Agda 证明... #Proof 我还是暂时不理解归纳证明

#media #life

是这道证明题

因为我当时没有 Agda 环境而且没看过 Agda 的语法参考，不敢随便修改这些东西，不要以为我只是抄了点代码然后啥都不理解

我好歹还抄了两节课...
我好歹对于 reverse 这种简单递归程序还分析了一会...

不准喷！不准喷！平时你们写那些 Android 应用.... Java 的 Web 后端程序我后来有时间了自然会学...

为了让你们不会喷我只会画个画没前途，特地发我在信息工程方面还会的一些东西...

我真的不是样样通样样松（虽然还并没有样样通）
我真的不是只会画个画，或者只会写个简单的程序或者算法什么的... 真的不是... 别喷

btw. 我这里说的 reverse 是 Haskell 里那种简单的 List reverse

使用 #Haskell 定义如下

reverse' :: [a] -> [a]
reverse' [] = []
reverse' (x : xs) = reverse' xs ++ [x]

当然也可以使用 fold 这种非常具有普适性的 operator 来写，那就是说

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
reverse'' :: [a] -> [a]
reverse'' = foldr (\x xs -> xs ++ [x]) []

题外话，我以为 infix operator (++) 的类型签名是

(++) :: [a] -> a -> [a]

但其实是

(++) :: [a] -> [a] -> [a]

结果出了很奇怪的类型问题，Couldn't match expected type ‘[a]’ with actual type ‘a’
而我作为 Haskell 初学者居然没有看懂是什么意思，即使人家连是哪里的问题都说出来了（In the second argument of ‘(++)’, namely ‘x’）
我真蠢...

main = do
print $ reverse' [1, 2, 3]
print $ reverse'' [1, 2, 3]

当然，其实你也可以认为 reverse' 和 qsort 类交换排序的函数是很像的

reverse' 的基线条件实际上是列表中只有一个元素的时候，这时候无需交换，递归的话直接返回列表就可以了，至于 reverse [] = []

其实，我们举个例子 reverse' [1, 2] 也即 reverse' 1 : 2 : []

我们来分析一下它的递归定义实际展开处理情况

reverse (x#1 : xs#[2]) = reverse xs ++ [x]
= reverse (2 : []) (1) ++ [1]

where (1)


  = reverse (x#2 : xs#[])
  = reverse ([]) (2)    ++ [2]

where (2)
  = reverse []
  = [] 

其实本来只有一个元素的时候可以不用考虑在 ++ [x] 什么的，直接返回即可（这个递归定义就是这个意思，因为最后一个 case 完全可以不需要再 [] ++ [x]，没必要），像这样
说到这个只是想大家平时多分析点递归定义，和 fold.pdf 那个 papper 上面那样，能由普通的递归函数定义推广到使用 fold 的定义这种能力

reverse'' :: [a] -> [a]
reverse'' xs
| length xs == 1 = xs
| otherwise = reverse'' (tail xs) ++ [head xs]

当然也可以拿 Scheme 写（没有意义，因为是等价的，我只是方便大家熟悉一下 Scheme）：

(define reverse
  (lambda (l)
    (cond
      ((eq? (length l) 1) l)
      (else (append (reverse (cdr l))  (car l))))))

（当然其实不是等价的，Scheme 上不应该 ++ [x] （reverse cons） 而只可以 (cons atom list) 正确的定义
（其实也不是只可以，你可以试试 (append '(1) 2)，不过不是所有标准 Scheme 列表处理函数都支持这种非正规的链表
这样也可以，我们再来看看这个

reverse'' [1, 2, 3]
= [;2] reverse'' [2, 3] ++ [1]

where reverse'' [2, 3]
= [;2] reverse'' [3] ++ [2]

where reverse'' [3]
= [;1] [3]

回溯回来就是 [3] ++ [2] ++ [1] 得 [3, 2, 1]