[M3devel] An awkward interaction of language properties

[Daniel Alejandro Benavides D.]

Hi all:
I would recall your attention on (just read the abstract if you may please modular soundness, that is to say 'safe' data abstraction and information hiding):
http://dl.acm.org/citation.cfm?id=570886.570888

What you can awkward features, I would call 'inherent' parametric polymorphism undecidability which is not at all a bad thing (remember ESC targets undecidable RT errors in all program universe), but in any case we can proof some properties because of that all program space you can still find errors if still are there (symbolic simulation is part of that technique I believe).

Thanks in advance



--- El mié, 22/2/12, Rodney M. Bates <rodney_bates at lcwb.coop> escribió:

> De: Rodney M. Bates <rodney_bates at lcwb.coop>
> Asunto: Re: [M3devel] An awkward interaction of language properties
> Para: "Antony Hosking" <antony.hosking at gmail.com>
> CC: m3devel at elegosoft.com
> Fecha: miércoles, 22 de febrero, 2012 12:45
> Yes.
> 
> 2.4.7: A complete revelation has the form:
> 
> REVEAL T = V
> 
> where V is a type expression (not just a name) ...
> 
> Whether this could be relaxed without introducing semantic
> problems would take
> careful thought, but I have been aware of how using what is
> popularly misnamed
> "name equivalence" for opaque types is needed instead of
> Modula-3's usual
> structural equivalence for other types.
> 
> On 02/21/2012 07:44 PM, Antony Hosking wrote:
> > Is that really true?  I would have thought that so
> long as the type name can be resolved to a concrete type
> then it would work.
> >
> > On Feb 21, 2012, at 3:59 PM, Rodney M. Bates wrote:
> >
> >> But a revelation must be a type constructor, not
> just a type name.
> >
> >
>