失踪人口回归, 几个月没写博客了.

最近跟着赵老师写了一些 Isabelle , 不过这个语言从2014开始不支持 Proof General, 而是用一个内嵌jEdit的IDE来开发. 总体感觉: 写起来很不舒服, 语言特性总感觉缺了些什么, IDE非常难用.

随着数理逻辑的不断学习, 对形式化这块能做的事情也比较怀疑. 证明了一些简单的数据结构/算法, 感觉 在证明难度上可能比OS的验证要简单, 快排/插排/堆/栈/队列都是可搞的, 之前被二分的验证卡了很久, 目前还是没有弄出来. (总的来说二分还是有点命令式, 用微软的 Dafny 可以轻松证明命令式的二分, 用一些循环不变式, 前置条件后置条件的方法, 直接用 Z3 可以自动证).

前不久在孔网入了一本二手的Python源码剖析, 因为从图书馆借来翻开一看就非常喜欢, 而图书馆那本已经破的要散架了, 惹不起, 想着坚持看完就剁手买了本二手, 成色很好, 和新的一样. 读了几个Python内建数据结构的实现, 看到了内存池, 字符串的Intern机制之类的东西, Python 为了弥补效率其实蛮拼的(然并卵). 之后几天比较忙, part II就看到函数调用为止, 还有一些参数机制没看完, 大体倒是对虚拟机的整个执行有所了解.

统计大作业和最近的PL作业都开始机器学习/大数据了.. 入坑学一发.