[isabelle-dev] Transparent/opaque module signature ascription

[Makarius]

On Fri, 12 Nov 2010, Brian Huffman wrote:

> So basically, you're saying that you normally don't care about 
> abstraction, except in the few special cases where you use abstype. 
> Maybe I do need to explain why abstraction is a good thing...

I do care about abstraction, and I did a lot of "narrowing" in the 
interfaces, but these things need to be done in a way that solves more 
real problems than introducing new ones by wild changes.  (Maybe you know 
the internal joke "SOMEthing went utterly wrong".)

Even if you have very abstract module interfaces (which are hard to figure 
out in the first place), there is a more fundamental lack of abstraction 
that is not addressed at all, namely how one works with the logic.

This starts with types typ and term, which are very concrete, but term is 
modulo aconv most of the time (I wonder how often this is violated in the 
code).  It continues when you refer to concrete logical constants and 
rules when building tools (decision procedures, packages etc.).  You are 
hooked to a particular concrete representation, and cannot easily 
transport the tool to another formulation of the same logical structure.

The local theory infrasturcture with its declarations plus morphisms 
addresses this to some extent, but very few tools are "localized" in that 
way.  At least the main specification packages are already "abstract" by 
being based on the Local_Theory interface.


 	Makarius