[bitc-dev] Type Classes: Pragmatics Questions

[Dominique Quatravaux]

I wrote:

 

>>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?)
>>    
>>
C Y wrote:

>I'm thinking that you would want the proofs to be human understandable
>up to the point where the proven system can run a proof checker ;-). [...]
>  
>
>In the end, if I'm understanding this, you have to just trust SOMETHING
>other than a computer for at least the beginning stages.  
>

Well, I believe that mechanical consensus ("the mechanical proof
verifier whose algorithm is described as text below, validates the proof
OK when implemented on most computer architectures in most languages")
is waaaay good enough. Way better anyway than any amount of human
verification, on proofs of any size and complexity.

Of course this leaves the mechanical proof verifier itself, and it's
underlying logic, to carefully inspect. But for some kinds of proof
systems at least (I'm thinking Coq again here), this can readily be done
inside a single brain with high assurance. Plus it's a fun exercise, a
mix between maths and philosophy - I wholeheartedly recommend "Gödel,
Escher, Bach: An Eternal Golden Braid" by Douglas R. Hofstadter, ISBN
0465026567, for more on this topic and others of extreme interest (to me
at least).

Preferring a lengthier, one-stage proof to this two-stage mechanism is a
bit like distrusting integer arithmetic theorems for doing finance IMHO
(a metaphor I lifted from the book). Although I fully understand Shap's
point that there *are* going to be people who "think" like that :-)

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

			Dominique Quatravaux <dom at kilimandjaro.dyndns.org>