软件基础

Hacker News 上怎么说

• xvilka · 2020 年

  用 Coq[1] 也能做到同样的事，它容易学[2]，活跃开发中[3]，文档也更好[4]。你还可以访问他们的讨论板[5]。关于常见的 Lean 与 Coq 之争以及所谓的“setoid 地狱”，你可以在他们的 GitHub 上读到长篇讨论[6]。 [1] http://coq.inria.fr/ [2] https://learnxinyminutes.com/docs/coq/ [3] https://github.com/coq/coq [4] https://softwar

  The same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq "war" and so-called "setoid hell" you can read a lengthy discussion on their GitHub[6]. [1] http://coq.inria.fr/ [2] https://learnxinyminutes.com/docs/coq/ [3] https://github.com/coq/coq [4] https://softwar

• kryptiskt · 2019 年

  《Software Foundations》（https://softwarefoundations.cis.upenn.edu）相当非正式且易懂，它不短，但非常有用。最好的通用入门书可能仍然是《Types and Programming Languages》：（https://www.cis.upenn.edu/~bcpierce/tapl/index.html）。这是一本好书，但它没有涉及依赖类型。

  Software Foundations (https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource. The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.

• nextos · 2020 年

  形式化方法的文献已经发展了很多。特别是有些很棒的广泛入门材料，使用 Coq 或 Isabelle： * https://softwarefoundations.cis.upenn.edu/ * http://www.concrete-semantics.org/ * http://adam.chlipala.net/frap/ 现在连 Little 系列也涵盖类型和证明了： * https://mitpress.mit.edu/books/little-typer * https://mitpress.mit.edu/books/litt

  The literature on formal methods has evolved a lot. In particular there is some great broad introductory material using either Coq or Isabelle: * https://softwarefoundations.cis.upenn.edu/ * http://www.concrete-semantics.org/ * http://adam.chlipala.net/frap/ Even the Little series covers types and proofs now: * https://mitpress.mit.edu/books/little-typer * https://mitpress.mit.edu/books/litt

• mcguire · 2017 年

  两个流派：* Coq/依赖类型。看看 Benjamin Pierce 等人的《Software Foundations》。所有内容都在线。也可以看看 Idris，Manning 出了一本好书。* 基于 SMT 求解器的现有语言验证。参见 SPARK/Ada（有一本好书但我不能……

  Two schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't…

• ojnabieoot · 2020 年

  我强烈建议看看“标准”的依赖类型理论和语言（甚至是没有依赖类型的证明助手），而不是试图一头扎进同伦论。学习依赖类型如何运作，会比试图补上代数拓扑的知识更有启发性。拓扑学与形式逻辑之间的联系固然有趣，但我认为你会……

  I would strongly recommend looking at “standard” dependently-typed theories and languages (or even proof assistants without dependent types), instead of trying to plunge into homotopy theory. Learning how dependent types work will be much more illuminating than trying to catch up on the algebraic topology. While the link between topology and formal logic is certainly interesting, I think you’ll be

• benrbray · 2021 年

  另一个不错的参考是 Loh 2001 的《Introduction to the Dependently-Typed Lambda Calculus》[1]，它也介绍了一些 PLT 记号，还有 Pierce 的教科书 [2]，它有一个经过形式化验证的精神续作 [3]。 [1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/inde

  Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3]. [1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/inde

正在加载完整评论……