duangsuse::Echo

#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)

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

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