Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??

Eric Allen wrote

> But since most proofs of language properties are written over toy 
> models that are supposed to capture the relevant features of a larger 
> language, and since a human determines the relevant features, 
> machine-checked proofs do not guarantee that nothing was missed.

I didn't say they guarantee that the real thing works as expected - but
machine checked proofs increase confidence considerably. In particular if the
informal proof says "this case is like the others."