[POPLmark] Meta-comment

[Karl Crary]

You make an interesting point.  In fact, all of the systems under 
discussion have huge TCBs when compared against what the Princeton FPCC 
project uses.  (The difference between, say, Twelf and Isabelle is small 
when compared with the difference between FLIT and anything else.)  And 
the Princeton guys paid a significant price to get there, first by 
implementing FLIT, and more importantly by doing their entire 
development in a manner that FLIT could verify.

The question is, are expressiveness and small-TCB really in conflict?  
Obviously they are today, with Twelf on one end and FLIT on the other.  
But they don't have to be.  There's no reason why Twelf (or Coq, 
Isabelle, etc.) couldn't write out a FLIT-checkable proof that 
summarizes its reasoning process.  Carsten and I are hoping to start 
work on this soon.

So there is definitely work to be done, but the issue is entirely 
surmountable, I think.

    -- Karl


James Cheney wrote:

>
>In addition to supporting tactics and user interactive proof, the three
>systems Dan mentioned (and others) also have very small "trusted theory
>bases" and small "trusted computing bases".  By "trust", I mean anything
>that cannot be checked.  That is, the mathematical foundations of these
>logics are small, standard, and has been exhaustively studied, the
>type/proof checking algorithms are well understood (and in many cases
>have been formally proved correct in some other system), and as long as
>you stick to the system's methodology (e.g., defining structures in
>terms of existing structures rather than introducing possibly-
>inconsistent axiomatizations in Isabelle/HOL etc), you know that what
>you are doing is consistent with a mathematical foundation that many
>people have studied and attempted to poke holes in, and failed.  
>
>  
>
...snip...