florian.haftmann at informatik.tu-muenchen.de
Wed Jan 21 09:44:25 CET 2009
> wrt to d) and e) (Users/Developers, HOL is difficult).
> This theory is for now a "using" HOL, but of course I want to develop it
> in a manner that it could become part of HOL.
> The situation you mention in d) and e) has not to be this way and we
> should not take it for granted that HOL is complex to develop etc. The
> social and psychological consequences are not very nice if it becomes a
> rule (my opinion).
I share your concerns, though I would see the subtleties of HOL rather
technical consequences than a "rule".
> Isabelle/HOL is remarkably more user friendly than many other system.
> All this effort of the past decades seems to have negative back effects
> in the past years: Many Developers stand before complex situations
> nobody or sometimes only one understands. Don't you think it is time to
> invest in a more developer-friendly Isabelle/HOL ?
Not sure whether user-friendliness means less developer-friendliness.
Whether the situation became worse in the past years -- in my view it
got even better, but this may be subjective due to my experience.
Perhaps the focus of problems shifted.
> If typerep is mainly used in connection with code-generation (as I
> understand) isn't it an option to generate all these instances when you
> call any code-generation facility? Or even in prior step e.g. called
This is even worse: in the first case, you won't be able to join any
(!) two theories which invoke code generation since you have a lot of
unredeemable duplication. The problem with the latter case is: there is
*never* such a point.
> Besides, I don't object to the idea of typerep at all, I am just
> confused why the names clash? (Wasn't this the problem). In other words
> is this problem unavoidable, so that one needs a hard
> discussion/decision like typerep or no typerep?
The problem is: you can instantiate every type class only once to a
particular type. There is no way to get around.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev