isarmathlib-devel
[Top][All Lists]
Advanced

[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.




reply via email to

[Prev in Thread] Current Thread [Next in Thread]