不必一次读完。每一段路径,都为下一段准备一个必要的概念。
先理解状态如何表示、操作如何改变状态,再把计算写成线路。
认识语言的不同层次,理解量子资源为什么需要类型约束。
把程序解释为状态上的变换,为比较和推理程序建立共同基础。
将程序性质写成断言,了解证明系统及其工具支持。