程序即证明

函数式编程语言OCaml

• OCaml的类型系统
  • 静态类型
  • 强类型
  • 类型检查
  • 类型推断
  • 多态
  • 主类型
• 类型系统的好处
  • 可以形成文档
  • 可以实现抽象
  • 可以提高编译程序的效率

使用OCaml实现一个小型编程语言