Pluto: a first concurrent web server in Gallina | Hacker News Reader

Pluto: a first concurrent web server in Gallina

coq-blog.clarus.me

58 pointsp4bl09 comments

Reminds me of Lemmachine, which was written in Agda (since i'm a Haskeller i gravitated towards that). I wonder if Lemmachine's still alive... /me looks

edit: not so much.

It's unclear what the grand scheme is here. Why using Coq instead of OCaml? How are the theorem proving of Coq used and to prove what? What do we expect from a web server anyway?

It is probably an interesting project but I don't see anything else on their website that witnesses more than the fact that they can write monadic code.

"It is a research project which aims to apply the pure and dependently typed Coq language to system programming, with inputs/outputs and fine grained concurrency in mind. … We try to develop new programming techniques with an extremist and purely functional approach, in the hope to lead to safer systems."

> The implementation of this DSL is two folds. In Coq, a run function gives an executable semantics of the computations. The existence of an executable semantics is an improvement over other works which only give unrealized axioms for I/Os effects

Also

> We can also question the correctness of the compilation to OCaml, or whether the run function in Coq is faithful to the extracted code. We have no formal proof, but we designed the system with correctness in mind.

So the `run` function lives in their general OCaml extraction DSL [0] and produces a provable semantics (the first fold) and an extracted OCaml program (the second fold) which are assumed today to be equivalent so that proofs on the first fold can be transported to properties about the second.

The run function looks like

    Fixpoint run 
      {sig : Signature.t} 
      {A : Type} 
      (call_backs : CallBacks.t sig)
      (mem : Memory.t sig) 
      (outputs : list Output.t) 
      (x : C.t sig A)
      : option A * CallBacks.t sig * Memory.t sig * list Output.t

which looks like a pure model of mutable typed memory, continuations via callbacks, and message passing.

[0] https://github.com/coq-concurrency/system

Check the Future Work:

"We learn many things writing a realistic example of a web server in Coq, especially in the way of implementing side effects. We also shown that it is possible to use Coq as a programming language to write interactive and concurrent softwares.

"Our main goal now is to extend our DSL of computations with a specification and a certification mechanism. We would like to write a specification of the non-purely functional part of our web server and prove its correctness, exploiting the unique ability of Coq to marry proofs and programs."

One of the ways of approaching a dependently-typed project (in my limited experience) is to start by building an otherwise-not-especially-typeiferous, but working, version, then backfilling the proofs necessary for correctness. This is particularly useful if you're new to the technology or (as in this case) not sure how exactly it's going to work.

"Note: Pluto is also the only planet discovered and undiscovered by the Americans."

As an aside, the way that's put is just...sad.

And not true. The IAU (an international organization) reclassified Pluto when they settled on a common definition of planet.

Yeah, I don't want to smear the work of good people. Neil deGrasse Tyson gets/got a surprising amount of hate mail from children due to his involvement in the definition of 'planet' and the reclassification, and man, he seems like a kind and thoughtful person. Obviously, there are people who wish to see Pluto be classified a planet that don't want good people to get hate mail from children, but this isn't the type of thing that should be "sad" or even controversial.

A world where classification of astronomical objects is cause for widespread controversy sounds kind of awesome to me.

Reply on news.ycombinator.com