[bitc-dev] Type Classes: Pragmatics Questions

[Dominique Quatravaux]

Jonathan S. Shapiro wrote:

>Note, however, that the "proven to terminate" qualifier is significant,
>and that this sharply restricts the space of programs that can be
>handled with this technique.
>
There are also other techniques such as Cousot's abstract interpretation
(that I talked about with you in private a while ago).

> Also, the monadic state transform can make
>human understanding of the proof process much harder.
>  
>
You mean that on top of providing the world with the perfect OS, you are
going to ensure that it's proof is legible to students ?! Wow. But is
that really a necessity? (Wouldn't trusting the proof checker be enough?)


-- 
<< Tout n'y est pas parfait, mais on y honore certainement les jardiniers >>

			Dominique Quatravaux <dom at kilimandjaro.dyndns.org>