[e-lang] Defensive consistency and integer overflow

[David Wagner]

Mark Miller writes:
>For example, given:
>
>    BigInteger a;
>    BigInteger b;
>
>then
>
>    a + b
>
>would expand to
>
>    a.add(b)
>
>Is this what you had in mind? Is it unwieldy for any reason, boring or
>otherwise?

Yes, that's basically what I had in mind, possibly along with some
promotion rules so that (for instance) adding an "int" and a "BigInteger"
gives you a "BigInteger".

The unwieldiness I had in mind is the issues associated with
source-code transformation and its effect on existing Java tools
(IDEs, debuggers, build tools, etc.).  I presume .java files would be
generated automatically from .joee files, and the programmer would only
be expected to look at the contents of the .joee files.  What changes
to Eclipse/IntelliJ/etc.  would we have to make to support this kind of
programming?  What would be the impact on debugging if line numbers (e.g.,
in stacktraces) refer to .java files rather than the .joee files that
the developer writes?  How easy would it be to write a source-to-source
transformer that stays up to date with new versions of the Java language?
All of this seems like mundane engineering stuff, so perhaps it is not
worth mentioning, but I don't know whether the annoyance of this would
outweight the security benefits of easy-to-use BigIntegers.

Yup, the attractiveness of C# as a basis for an objcap language hasn't
escaped my notice.


P.S. In Java, with or without extensions to reduce the notational overhead
of using big integers, there's a minor bit of ugliness: BigInteger is
not a final class.  This means that code that receives a BigInteger "a"
cannot rely upon the expression "a + b" to actually perform addition,
unless the code somehow has knowledge of the exact runtime type of "a".

At a recent meeting with Adrian and Ping, they raised the suggestion
that perhaps we should introduce a notion of 'honorarily final' into
Joe-E.  The idea: add a marker interface, with some name like Library or
Standard or Final or Semifinal.  Some library classes like BigInteger
could be marked honorarily Library.  The Joe-E verifier would prevent
Joe-E classes from subclassing any Library class.  Other Java library
classes might still be allowed to subclass a Library class, but because
we know that Joe-E code cannot do so, we can rely upon the behavior of
objects of that type.

The advantage of this idea is that it would allow Joe-E code to use
the static type system to establish trust in the behavior of objects
it receives.  The disadvantage is that we would have to make a decision,
for once and for all, about which classes are marked Library.  If some
Joe-E apps would like to be able to subclass BigInteger and others would
like to be able to rely upon the impossibility of subclassing BigInteger,
this approach becomes problematic.

Ping also raised the suggestion of a programming discipline where any
time a method accepts a parameter of non-final type, the programmer should
annotate it (e.g., @nonfinal) to help indicate that the behavior of that
parameter cannot be relied upon.  Then one could build a lint-like type
that warns about any method parameters whose type is non-final and that
doesn't have a @nonfinal annotation.  This would not make sense for
inclusion in the Joe-E verifier but might be an interesting idea for
a caplint.