[clean-list] Sparkle and ABC-code

[Maarten de Mol]

> Maarten de Mol wrote:
> Unfortunately, there is no manual for Sparkle available.
>
> In that case I will just ask: Sparkle is able to convert full Clean code
to
> desugared Clean. The Sparkle website only excludes I/O-code. Does that
mean
> that proofs *can* be generated and checked for functions that include
> ABC-code? After all ABC-code, included in "code {...}" *is* part of the
> official Clean syntax, right?

It is part of the Clean syntax. But I don't think it is also part of the
Clean *semantics*.

How SPARKLE handles ABC-code: It doesn't.
Instead, it recognizes special functions from the standard environment
(currently by looking at the combination (name,module)) and assigns a
predefined meaning to these. All functions written in ABC-code in the
standard environment are recognized this way.

Other functions written in ABC-code will not be recognized and cannot
be compiled by SPARKLE.

By the way: there is room for improvement here, because we do have
an ABC-interpreter available. Assigning a proper semantics should
be possible for a subset of ABC-code.

> Regards Erik Zuurbier
>
> (On the other hand, if you view ABC-code as an official part of the Clean
> language, Clean's claim to be 'pure' seems to be unjustified.)

Greetings,

Maarten de Mol