A blog engine written and proven in Coq • Hacker News Board

Re: A blog engine written and proven in Coq

#51

Post by pseudonom- » Thu, Feb 12, 2015, 7:02 PM UTC

adultSwim wrote: post #44

allan_s wrote: post #31

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…

It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions. So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list an…

My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).

Re: A blog engine written and proven in Coq

#52

Post by vilhelm_s » Thu, Feb 12, 2015, 9:41 PM UTC

pseudonom- wrote: post #51

adultSwim wrote: post #44

Earlier quoted context omitted.

It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions. So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list an…

My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).

Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)

Re: A blog engine written and proven in Coq

#53

Post by smadge » Fri, Feb 13, 2015, 12:28 AM UTC

wernercd wrote: post #43

tpaksoy wrote: post #19

Earlier quoted context omitted.

It's not just that "Coq" might sound like "cock", but a "Coq blog" just sounds even funnier...

I just hate to think of the poor girl/woman who decides she loves the framework...

Why does it have to be a girl/woman? Why would it be any different for a boy/man to say they love Coq?

This actually happened to me. A classmate said something about Coq, and I did a double take. He explained it was a language, but for a second he got my hopes up.

Re: A blog engine written and proven in Coq

#54

Post by clarus » Fri, Feb 13, 2015, 11:01 AM UTC

pja wrote: post #11

__alexs wrote: post #10

Earlier quoted context omitted.

> that doesn't seem an unreasonable assumption to make in this case Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too. Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?

I don't know whether this particular proof models IO timeouts - might have a poke at it and see what it's doing if I have time later. More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it'…

Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...

In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.

Re: A blog engine written and proven in Coq

#55

Post by clarus » Fri, Feb 13, 2015, 11:09 AM UTC

kriro wrote: post #8

hrjet wrote: post #5

The last line threw me off: > an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls. System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?

Without reading the sourcecode/proof (bookmarked for later) my guess is that it simply means something along the lines of "the user cannot execute code a la eval". So basically the user can do exactly the specified actions and nothing more.

By "system call", we do not mean "kernel call" but more "call to the system" in a broader sense, that is from the program to its environment (it could be the OS or other libraries). We should probably use another word since this is confusing.

More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...

Re: A blog engine written and proven in Coq

#56

Post by clarus » Fri, Feb 13, 2015, 11:13 AM UTC

legulere wrote: post #9

Is it also proven that no cross-site-scripting attacks are possible?

No, nothing is done about it, the post contents are not even escaped to generate safe HTML.

Re: A blog engine written and proven in Coq

#57

Post by clarus » Fri, Feb 13, 2015, 11:20 AM UTC

allan_s wrote: post #36

sun_machine wrote: post #35

Earlier quoted context omitted.

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.

I understand better, so basically before doing anything you will first need to define what each "part" of the language "means" in term of "logical operation" (like what does the dot operator '.' means in PHP, which type it accepts and it transforms them etc) Right ?

Coq itself is already a programming language, but pure in the sense there cannot be any side effects (like IOs). For this pure part there are already an interpreter and a compiler to OCaml, Haskell or Scheme.

To extend Coq with IOs you need to define each new external call. This is basically what is done in the files https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extract...

Re: A blog engine written and proven in Coq

#58

Post by eli_gottlieb » Fri, Feb 13, 2015, 2:34 PM UTC

mcmancini wrote: post #40

adultSwim wrote: post #34

Earlier quoted context omitted.

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.

Winner winner chicken dinner. I read the preface and this sounds exactly like what I was looking for. Many thanks!

I worked through it last year and had a great time. Enjoy!

Re: A blog engine written and proven in Coq

#59

Post by chriswarbo » Fri, Feb 13, 2015, 5:34 PM UTC

more_original wrote: post #25

eli_gottlieb wrote: post #17

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,…

> 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, but one cannot execute a Turing Machine for an unbounded number of steps.

I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive step function?

Re: A blog engine written and proven in Coq

#60

Post by more_original » Sat, Feb 14, 2015, 3:25 PM UTC

chriswarbo wrote: post #59

more_original wrote: post #25

Earlier quoted context omitted.

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,…

> 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, but one cannot execute a Turing Machine for an unbounded number of steps. I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive st…

You can extract lazy values that represent infinite data. For example, you can define the stream of the factorial numbers as follows.

  CoInductive Stream (T: Type): Type :=
    Cons: T -> Stream T -> Stream T.

  Fixpoint fac(n : nat): nat := 
    match n with
    | 0 => 1
    | S n => n * (fac n)
   end.
 
  CoFixpoint facs : nat -> Stream nat := 
  fun n =>
   Cons (fac n) (facs (n+1)).

  Definition fs := facs 0.

It's extracted to the following Haskell code:

  data Stream t =
    Cons t (Stream t)

  fac :: Nat -> Nat
    fac n =
    case n of {
     O -> S O;
     S n0 -> mul n0 (fac n0)}

  facs :: Nat -> Stream Nat
    facs n =
    Cons (fac n) (facs (add n (S O)))

  fs :: Stream Nat
    fs = facs O

It should be possible to define a function that given a Turing Machine returns the stream of its states analogously. But to actually compute the states in Haskell you would have to write a driver function that actually forces their computation one after the other.

Even without corecursive data, you can define a function that for a given TM returns a function of type nat->state, which computes the state of the TM after k steps. In a way this value also represents the whole, possibly infinite, computation of the machine.