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 <[EMAIL PROTECTED]> wrote:
On Mon, Dec 8, 2008 at 4:01 AM, Yuh-Ruey Chen <[EMAIL PROTECTED]>
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
[email protected]
https://mail.mozilla.org/listinfo/es-discuss
_______________________________________________
Es-discuss mailing list
[email protected]
https://mail.mozilla.org/listinfo/es-discuss
