Re: Dpkg in Ocaml

[Claudio Sacerdoti Coen <sacerdot@CS.UniBO.IT>]

 Hi,

> Well, i am not really a coq user, so i don't know if this is actually
> feasible. I was told it is possible though. 

 well, as a Coq user I think that it is _A_LOT_ of work to do that. Moreover:

  1. dpkg is not really a critical application (no lost of human lifes,
      no lost of money, etc.)
  2. it is not even exactly clear to me _what_ do you want to prove.

 For example, the FS operations of the kernel of Linux have been proven
 correct in Coq, in the sense that it has been proven that no process can
 read/write/execute a file if it has no right to do that. What do you want
 to prove on the implementation of dpkg? It there is something interesting
 to prove, maybe (maybe!) it could be worth the effort.

 					 Cheers,
					 C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail: sacerdot@cs.unibo.it
http://caristudenti.cs.unibo.it/~sacerdot
----------------------------------------------------------------