3 ms·

Do you have any good resources for someone wanting to understand that a bit more? I'm super interested but this all seems a bit hard to get my head around..

kmicklas 10y ago
I don't know that much about machine learning and have only briefly surveyed the landscape of research on machine learning for theorem proving, but if you want to learn about the current state of the art in verified programming it's probably Adam Chlipala's book: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
wolfgke 10y ago
If you want to have a look into the state of the art of axiomatic systems that can be (and have been) used for proofs that can be checked by a computer, it surely is not a bad idea to read the Homotopy Type Theory (HoTT) book, which is freely available at > https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ If you prefer a more "established" way: Common systems for computer-checked proofs are Isabelle/HOL, Coq and Agda (the latter is often commonly "only" called a programming language, but also has been used for this purpose). For Isabelle/HOL (https://isabelle.in.tum.de/ https://isabelle.in.tum.de/) I only know the official documentation as a resource: https://isabelle.in.tum.de/documentation.html https://isabelle.in.tum.de/documentation.html For Coq (https://coq.inria.fr/ https://coq.inria.fr/) a good book book is "Coq'Art: The Calculus of Inductive Constructions" by Yves Bertot and Pierre Castéran. Unluckily it is not (legally) freely available. Finally for Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) I recommend reading Ulf Norell's PhD thesis "Towards a practical programming language based on dependent type theory" and the more introductory paper "Dependently Typed Programming in Agda". Both texts are available at http://www.cse.chalmers.se/~ulfn/ http://www.cse.chalmers.se/~ulfn/
- cmrx64 10y ago
  The best resource for getting started with Isabelle/HOL is http://www.concrete-semantics.org/ http://www.concrete-semantics.org/. Freely available.
- yaantc 10y ago
  A good resource to learn Coq is "Software Foundation": https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html It teaches the foundation of software with simply typed lambda calculus, but also teaches how to use coq and use it for software verification. I found it more approachable than Coq'Art, which is also very good but I'd suggest starting with SF first then read Coq'Art.
nickpsecurity 10y ago
These two are the common resources recommended for this sort of thing: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://concrete-semantics.org/ http://concrete-semantics.org/ Most work in the field is using Coq or HOL. The second one applies to seL4. I don't think it will help you understand it much given the complexity of that work. You might have better luck looking at Myreen's verifications of LISP 1.5 or CakeML in Isabelle/HOL. Or even their verification of HOL itself.

kmicklas 10y ago

I don't know that much about machine learning and have only briefly surveyed the landscape of research on machine learning for theorem proving, but if you want to learn about the current state of the art in verified programming it's probably Adam Chlipala's book: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/

wolfgke 10y ago

If you want to have a look into the state of the art of axiomatic systems that can be (and have been) used for proofs that can be checked by a computer, it surely is not a bad idea to read the Homotopy Type Theory (HoTT) book, which is freely available at > https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ If you prefer a more "established" way: Common systems for computer-checked proofs are Isabelle/HOL, Coq and Agda (the latter is often commonly "only" called a programming language, but also has been used for this purpose). For Isabelle/HOL (https://isabelle.in.tum.de/ https://isabelle.in.tum.de/) I only know the official documentation as a resource: https://isabelle.in.tum.de/documentation.html https://isabelle.in.tum.de/documentation.html For Coq (https://coq.inria.fr/ https://coq.inria.fr/) a good book book is "Coq'Art: The Calculus of Inductive Constructions" by Yves Bertot and Pierre Castéran. Unluckily it is not (legally) freely available. Finally for Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) I recommend reading Ulf Norell's PhD thesis "Towards a practical programming language based on dependent type theory" and the more introductory paper "Dependently Typed Programming in Agda". Both texts are available at http://www.cse.chalmers.se/~ulfn/ http://www.cse.chalmers.se/~ulfn/

cmrx64 10y ago
The best resource for getting started with Isabelle/HOL is http://www.concrete-semantics.org/ http://www.concrete-semantics.org/. Freely available.
yaantc 10y ago
A good resource to learn Coq is "Software Foundation": https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html It teaches the foundation of software with simply typed lambda calculus, but also teaches how to use coq and use it for software verification. I found it more approachable than Coq'Art, which is also very good but I'd suggest starting with SF first then read Coq'Art.

nickpsecurity 10y ago

These two are the common resources recommended for this sort of thing: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://concrete-semantics.org/ http://concrete-semantics.org/ Most work in the field is using Coq or HOL. The second one applies to seL4. I don't think it will help you understand it much given the complexity of that work. You might have better luck looking at Myreen's verifications of LISP 1.5 or CakeML in Isabelle/HOL. Or even their verification of HOL itself.