[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Isarmathlib-devel] [isabelle] Untyped formalized systems are wrong
From: |
Slawomir Kolodynski |
Subject: |
Re: [Isarmathlib-devel] [isabelle] Untyped formalized systems are wrong (blog post) |
Date: |
Sat, 9 Jul 2011 03:26:13 -0700 (PDT) |
Indeed discussing which foundation is best is a bit like discussing religions.
The best approach is to try this, try that, and then choose what is best suited
for your mind set and problem domain.
As for the “long, dependent on arguments qualifiers on every operation” I think
this is more of a presentation problem than the foundation problem. Humans are
very good at figuring out certain details from context. If those details don’t
contribute to understanding of the proof they should be suppressed by the
presentation layer. That fixes the problem on the reader side. On the writer
side it is more difficult to fix and it may be unavoidable to tell the proof
assistant exactly what you mean.
Many people think it is a good idea to layer some type system on top of untyped
set theory, see Sebastian Reichelt’s HLM and ZPC by Jeremy Bem.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- Re: [Isarmathlib-devel] [isabelle] Untyped formalized systems are wrong (blog post),
Slawomir Kolodynski <=