[bitc-dev] Type Classes: Pragmatics Questions

Jonathan S. Shapiro shap at eros-os.org
Mon Aug 1 10:46:35 EDT 2005


On Mon, 2005-08-01 at 19:41 +0200, Dominique Quatravaux wrote:
> > 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?)

I'm not worried about convincing people like *you* -- heck, you trust me
already. :-)

Okay. Jokes aside, my problem is that I'm a lousy researcher because I'm
an engineer at hard. It would be possible to do all of this work,
generate a non-engineerable and non-repeatable result, write a bunch of
papers, and declare victory. That would be a typical research scientist
approach.

I'm not satisfied unless I have a solution that I think will allow us to
successfully iterate and reuse in successive releases.

To accomplish that, it needs to be readable.

shap



More information about the bitc-dev mailing list