Re: Dpkg in Ocaml

[Sven Luther <luther@dpt-info.u-strasbg.fr>]

On Thu, Dec 05, 2002 at 10:58:58AM +0100, Claudio Sacerdoti Coen wrote:
>  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.)

  Well, not directly at least. But i guess that if you use (and update)
  a critical box with dpkg, then it quickly makes dpkg critical, does it
  not ?
  
>   2. it is not even exactly clear to me _what_ do you want to prove.

  That is the true question, sin't it ? 

>  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.

Well, we have specs in the policy documents about what dpkg should do
and not do, what you could prove is that the dpkg implementation does
exactly what is in the specs, not less, not more, and that it does not
break, loop forver, whatever else. I guess some of this you already get
by just writing stuff in ocaml. As a side effect you could prove that
the policy specs is true to its goal and not buggy in itself.

Anyway, like you said, it would be lot of work, but fun to do.

Another thing that may benefit from some rigorous thinking is the new
debian election stuff being discussed on debian-vote. I think a rigorous
proving would cut short a lot of the discution going along there.

Friendly,

Sven Luther