类型系统是实现与规范之间的桥梁

花了比预想中更多的时间研究SquirrelFS和其所基于的Soft Updates。

状态机是很多形式化验证的基础，几乎可以视作验证模型的「中间表示」。如果采取了手动对应（未验证的）实现和（验证了的）规范的手段，那么其中的一部分工作量就出自对于验证模型的状态转移的映射。

类型系统，具体到Rust类型系统，可以辅助确保其中一个重要属性：状态转移的完备性。验证模型中列出的状态转移就是全部可能的状态转移。如果有多的（或者反过来说，程序员无法证明不会有多的），Rust编译器会抓到并报错。

当然了，这不是什么定理或者逻辑系统，只是一种工程方法论。没有什么拦着程序员在实现中写出（允许）额外的状态转移（的类型），只是这种失误会以非常显而易见的（愚蠢）形式呈现出来。

接下来要看看能不能对我们更熟悉的分布式协议做采用了这种手段的「用户友好型」验证。先写些规范（并验证之），然后在（Rust）类型系统里面尽量多的编码规范中的细节。具体是什么细节（目前）并没有精确的定义，只要能在（以各种方式）与规范分道扬镳的时候让编译器报错就行了。

总之先学一下Alloy。昨天被ℒ问到Alloy和TLA+之间如何取舍，做了一些调研以后，不但依旧没法决定二者孰优孰劣，甚至还又发现了P，让人有些哭笑不得。多些参考总归是好的吧，就是在眼下有点着急的境况下却还是不得不先做些探索性的工作，有点沉不住气了。

---

拿pyglet写起了2048。非常符合我需求的一个图形库，哪怕综合考虑各种编程语言都属于是出类拔萃。为什么才发现呢。

对动态成员系统的（严肃的）形式化验证企划和去实习的打算都搁置着。

先前的cover项目目前被转换成了上面所描述的样子，原本的关于可验证逻辑时钟的技术研发（主要是零知识）被视作是其后续工作而一定程度上冻结了。这样说来，PhD阶段所做的四个项目也许变回了三个。

𝒦在几天之内有了不少新计划。对SNN的并行化编码和医学方面的应用都有了投期刊的打算。一个关于SNN鲁棒性的研究也许会在接下来开展。商业企划虽然受到了老板的鼓励但是还是先离开一下。AAAI过了第一轮，祝她能走得更远。