Allen's lambda syntax proposal

Brendan Eich brendan at mozilla.com
Mon Dec 8 09:16:01 PST 2008


The auditors idea is good; we've talked about it in the context of  
Harmony.

Of course, ES4 had optional types, but over time ES4 lost the idea of  
a normative optional static checker. It's not clear on the web *when*  
you check. Cormac Flanagan proposed checking "when it seemed like a  
good time" -- when script and page loads stabilized into some web app  
cohort of sources that seemed not to be loading more code at the moment.

Optional offline static analyses can be powerful tools. They don't  
even need soundness to be useful -- Mozilla's experience in C++ bears  
this out (http://blog.mozilla.com/tglek/). The same trade-offs may  
apply to a Harmonious optional annotation system, if it's used well in  
real code.

/be

On Dec 8, 2008, at 8:36 AM, Mark S. Miller wrote:

> On Mon, Dec 8, 2008 at 7:20 AM, Jon Zeppieri <jaz at bu.edu> wrote:
> On Mon, Dec 8, 2008 at 4:01 AM, Yuh-Ruey Chen <maian330 at gmail.com>  
> wrote:
> > Breton Slivka wrote:
> >> 2) It would be really nice to have a callable value that was
> >> garaunteed not to have side effects.
> >
> > This little comment got lost in the recent deluge of emails, but I  
> too
> > would really like some mechanism to avoid or see if a function  
> causes
> > side effects (and not just mutability).
>
> Without a static type system, there's very little you can do.
> Sure, you could abandon the proof requirement and turn it into an
> assertion, so that if F is annotated as "mutation-free" and if, at
> runtime, it tries to perform an assignment, an exception is thrown.
> But this doesn't work so well for other computational effects.
> Throwing an exception itself is an effect, and it would be pointless
> to throw an exception when your code illegally attempts... to throw an
> exception.
>
> Non-termination is an effect, and it's notoriously immune to runtime  
> checks.
>
> I/O effects are possibly the most interesting from a practical
> perspective, but they're outside the scope of the ES standard.
>
> E's auditors <http://www.erights.org/elang/kernel/auditors/> <http://wiki.erights.org/wiki/Guard-based_auditing 
> > are a mostly non-static approach that can verify many properties,  
> including side effects per se including IO effects, but not  
> including throws and non-termination. Joe-E's similar, but non- 
> extensible and static auditor system <http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf 
> >, has been used to verify some nice purity properties.
>
> I am not ready to propose any such thing for Harmony at this time.
>
> -- 
>    Cheers,
>    --MarkM
> _______________________________________________
> Es-discuss mailing list
> Es-discuss at mozilla.org
> https://mail.mozilla.org/listinfo/es-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20081208/3b36667e/attachment.html>


More information about the Es-discuss mailing list