感觉第一节课都差不多
推荐了Software Foundations，搜了一圈发现非常劝退....但还是磨磨蹭蹭看完了Lists
书上说不建议贴答案和题解，那就不贴了吧（
developing general abstractions, or building blocks, for solving problems, or classes of problems. Also considers software behavior in a rigorous and general way, to prove that programs enjoy properties
当我们提及程序的正确性时，我们在谈论什么？
- How to describe meanings of programs? 含义
- How to describe properties of programs? 性质
- How to reason about programs? 推理
- How to tell if two programs have the same behaviors or not?
- How to design a new language?
- How to build Bug-Free Software?
现在的软件也越来越复杂
- Multi-core concurrency
- Embedded software, Limited resources
- Distributed and cloud computing, Network environment
- Ubiquitous computing and IoT
- Quantum Computing
测试的局限性
- 简单，容易自动化、流程化
- 无法保证一定没有bug
- 对并发(多核/网络)程序作用有限，发现的bug难以重现
- Testing shows the presence, not the absence of bugs. Dijkstra
对于Crash-Proof工作，如何证明？
- How to prove mathematically?
- How to define "crash"?
- How to prove a system is "crash-free"?
为什么要上这门课？
- 软件可靠性是目前严重的问题
- 是别人没有的优势
- 可以提升代码能力
- 更好地理解和比较编程语言
- 这门课很有挑战
课程内容
- 对现有语言的研究
- 讲一些定义程序行为的方法
- 讲一些证明程序性质的方法
- 如何定义性质
- 如何证明
Coq
- 可以自动化证明命题
- 可以自动化验证证明
- 我们不再需要信任证明，只需要信任证明工具，然后检验一个证明
也就是说，一个程序可以自带一个安全性proof，而运行环境自带的证明器用以验证，以此来保证程序是正确的