[Prev][Next][Index][Thread]
Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??
-
To: ericeallen@mac.com
-
Subject: Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??
-
From: nipkow@in.tum.de
-
Date: Mon, 18 Nov 2002 12:51:08 +0100 (MET)
-
Cc: types@cis.upenn.edu
-
In-reply-to: <DE01DB46-FA94-11D6-BE73-0003937325AC@mac.com> (message from Eric Allen on Sun, 17 Nov 2002 19:27:14 -0600)
-
References: <DE01DB46-FA94-11D6-BE73-0003937325AC@mac.com>
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."
Tobias