31–40 of 60 posts
It is written there's a Coq->OCaml compilation step. Would it be easily possible to have any Coq->other language (I'm mostly thinking about Rust) compiler ? Or do some properties of OCaml make it much easier (I mean "several order of magnitude") to implement than more 'common' dynamic languages like Php/Python/ruby ?
Earlier quoted context omitted.
In Coq all functions terminate. Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program of this type. If one allowed non-termination, then it would be easy to construct a program of any type (like in OCaml let rec f() = f() has type () -> 'a), so you could prove anything.
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover. In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that…
This is such a terribly badly named language for anyone in the UK!
Is there a good practical resource for learning about applying formal proof systems like Coq or Spin, but for those without a CS background? I'm interested in provably correct systems, but a lot of the material seems to be heavy on the theoretical side. I guess you could say I'm searching for the Art of Electronics , but for formal proofs.
To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is.
Highly recommend.
disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works. It is written there's a Coq->OCaml compilation step. Would it be easily possible to have any Coq->other language (I'm mostly thinking about Rust) compiler ? Or do some properties of OCaml make it much easier (I mean "several order of magnitude") to implement than more 'common' dynamic languages…
disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works. It is written there's a Coq->OCaml compilation step. Would it be easily possible to have any Coq->other language (I'm mostly thinking about Rust) compiler ? Or do some properties of OCaml make it much easier (I mean "several order of magnitude") to implement than more 'common' dynamic languages…
Coq is essentially a verification system and functional programming language all in one. The functional programming language that the proofs are based on has similar (identical in some places) semantics to OCaml. Remaining faithful to these semantics, especially in a verifiable way, quickly becomes herculean. Even formalizing the semantics of a language is a process that takes months.
Earlier quoted context omitted.
Technically speaking, corecursion allows for writing Turing-complete programs, including nonterminating programs. It just requires that you explicitly specify where you use nontermination and prove that each iteration yields a well-typed result.
Yes, one can represent non-terminating programs. One can represent Turing machines as data, after all. But one cannot write a Coq function that will fully execute such programs. Each well-typed Coq function, when applied to concrete arguments, will terminate in a finite number of steps. One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps,…
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
Earlier quoted context omitted.
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover. In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that…
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
Earlier quoted context omitted.
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover. In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that…
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
Is there a good practical resource for learning about applying formal proof systems like Coq or Spin, but for those without a CS background? I'm interested in provably correct systems, but a lot of the material seems to be heavy on the theoretical side. I guess you could say I'm searching for the Art of Electronics , but for formal proofs.
Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/current/index.html To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is. Highly recommend.
I read the preface and this sounds exactly like what I was looking for. Many thanks!