依赖类型认证编程

Hacker News 上怎么说

• tel · 2014 年

  想要学这方面的内容，我一向推荐 Pierce 的《Software Foundations》[0] 和 Chlipala 的《Certified Programming with Dependent Types》[1]，这两本网上都有免费版。不过我也在看《Coq d'Art》，非常喜欢……可惜这本书不太好找。[0] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html…

  For learning this sort of thing I always recommend Pierce's Software Foundations [0] and Chlipala's Certified Programming with Dependent Types [1] which are both available online for free, but I'm also reading through Coq d'Art as well and like it a lot... unfortunately it's harder to find. [0] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html…

• harveywi · 2016 年

  如果你对形式化验证编程的最新进展感兴趣，不妨关注一下 Adam Chlipala 的研究（尤其是 Bedrock [1]）。他的著作《Certified Programming with Dependent Types》是一个极佳的学习资源。Coq 一开始可能会让人望而生畏，因为它实际上把三门不同的编程语言揉在了一起：Gallina 是核心的纯函数式编程语言，Vernacular 是一种……

  If you are interested in recent developments in verified programming, you might be interested in looking at Adam Chlipala's work (in particular, Bedrock [1]). His book "Certified Programming with Dependent Types" is a fantastic resource. Coq can be daunting to start with because it is three different programming languages in one: Gallina is the main pure functional programming language, Vernacular is a language…

• ebingdom · 2021 年

  要我说，类型系统方面推荐的书就是它。类型理论方面，我推荐 Adam Chlipala 的《Certified Programming with Dependent Types》或者 Philip Wadler 的《Programming Language Foundations in Agda》。

  I'd say it's the recommended book for type systems. For type theory, I'd recommend "Certified Programming with Dependent Types" by Adam Chlipala or "Programming Language Foundations in Agda" by Philip Wadler.

• erichocean · 2016 年

  顺便说一句，我并不是数学出身，也没觉得用 Coq 有多痛苦。一旦我真的想要经过验证的代码，用 Coq 做事似乎就是最省力的路径，因为证明自动化的工具相当棒，尤其是如果你照着《Certified Programming with Dependent Types》[0] 里的方法来。 我还喜欢用 Alloy[1] 来摆弄逻辑数据结构的定义，交互式地……

  FWIW, I'm not mathematically-inclined and haven't found Coq to be painful to use. As soon as I really want verified code, doing stuff in Coq seems like the easiest path because the proof automation tooling is pretty great, especially if you follow the approach in Certified Programming with Dependent Types[0]. I also like Alloy[1] for messing around with logical data structure definitions interact

• jeremysalwen · 2017 年

  如果你真的想在“rock”之上构建，看看 Bedrock：http://plv.csail.mit.edu/bedrock/ 。别只证明你的程序内存安全，要证明它满足任意性质！（有点开玩笑，但这些工具真的很酷）。看看 http://adam.chlipala.net/cpdt/cpdt.pdf ，是个不错的入门。

  If you really want to build on "rock", check out Bedrock: http://plv.csail.mit.edu/bedrock/ . Don't just prove your program is memory safe, prove it satisfies arbitrary properties! (A bit tongue in cheek, but the tools are really cool). Check out http://adam.chlipala.net/cpdt/cpdt.pdf for a nice introduction.

• reycharles · 2013 年

  如果你想上手 Coq，有两个好资源。一个是 Benjamin Pierce 的 Software Foundations[sf]。还有 Adam Chlipala 的《Certified Programming with Dependent Types》[cpdt]。我觉得 [cpdt] 比 [sf] 更进阶，所以最好从 [sf] 开始，然后如果你觉得能接受挑战，再开始看 [cpdt]。 对于 Coq 作为软件工具，我的感受挺复杂……

  If you want to get started with Coq there are two good resources. One is Software Foundations[sf] by Benjamin Pierce. There's also Certified Programming with Dependent Types[cpdt] by Adam Chlipala. I would say [cpdt] is more advanced than [sf], so I think it's best to start with [sf] and then start on [cpdt] if you feel up for the challenge. I have mixed feelings about Coq as a tool for software

正在加载完整评论……