Re: Accept Anarchy
Victor Yodaiken (yodaiken@sphinx.nmt.edu)
Fri, 12 Aug 1994 10:28:53 -0600
On Aug 12, 9:52am, David McAllester wrote:
Subject: Accept Anarchy
>I do not think that developers will choose to build translators to and
>from raw set theory. Raw set theory does not maintain the "structure"
>of theorems. Structure is essential in heuristically guiding
>verification. For example, many verifications rely on type checking
>algorithms. Raw set theory does not distinguish types from other
>formulas.
Bravo. I'm no fan of complex type theories, but it is important to
realize that just because one _can_ encode a part of mathematics inside
another, it does not mean that one should.