Modern Eiffel
Helmut
The key features:
- Integration of functional and imperative programming into one
language (in a
similar manner as scala)
- Variable and routines with limited scope
- Richer types (e.g. immutable types) and type inference
- Completely type safe
- Assertions can be statically verified
- Powerful concurrency
http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/modern_eiffel.txt
Helmut
Parallel wait has been added to the concurrency chapter.
llothar
With useable i mean with libraries and not proof-of-concept minimal
classes.
Yosifov Pavel
What is needed: to fix strange syntax in the language.
Georg Bauhaus
Could you elaborate?
Helmut
I fully understand your point. But one has to make the things in the
right order. I have started the tecomp project with the thinking that
Eiffel is a mature language. During the implementation a lot of
inconsistencies with the current definition of the language emerged
(type safety, command query separation not enforced, no solution to
the framing problem, assertion language not powerful enough). I
realized that implementing a lot without fixing the deficiencies is a
waste of time (at least if I stick to my goal -- see below). I kept
the libraries deliberately small and tagged the compiler still
"beta" (the implementation is rather stable, but the language is not
stable) because non compatible language changes are inevitable. The
papers published are still for discussion, because Modern Eiffel still
needs some fine tuning.
ISE has already made the variant "implement fast, release and then
solve the language problems". But now they nearly cannot move forward.
They have paying customers who press them to make all changes backward
compatible. The effect: No progress in the language definition since
2005!
My overall goal: A verifying compiler (statically proof assertions)
for sequential *and* concurrent programs based on a sound langugage
definition. ISE offers currently a implementation of concurrency
concept (SCOOP) which in my opinion is rather immature (I talk about
the concept, not the implementation). This is released too early for
production code (hopefully they tag it as beta in order to avoid that
no production code uses it).
llothar
> I fully understand your point. But one has to make the things in the
> right order.
And i don't think your order is the right order. Look at google go!
It's a very simple language with no generics and exceptions. But it
has people to try it out and give feedback because it can be used at
least for small toy programs.
> ISE has already made the variant "implement fast, release and then
> solve the language problems". But now they nearly cannot move forward.
> They have paying customers who press them to make all changes backward
> compatible.
And you have not. So you can use design by evolution.
> My overall goal: A verifying compiler (statically proof assertions)
> for sequential *and* concurrent programs based on a sound langugage
> definition.
I doubt that anybody outside academics really need and want this.
> ISE offers currently a implementation of concurrency
> concept (SCOOP) which in my opinion is rather immature (I talk about
> the concept, not the implementation). This is released too early for
> production code (hopefully they tag it as beta in order to avoid that
> no production code uses it).
It is released after how many years - 15? - where it only existed in
theory. And it is a real stinker for all current implemented
multithreading programming.
And again command-query separation and mulitthreading does not work
together very well.
By the way: I like many of the features of modern Eiffel, one missing
is to modernize the exception handling. A try catch finally style
should be used.
Georg Bauhaus
>> My overall goal: A verifying compiler (statically proof assertions)
>> for sequential *and* concurrent programs based on a sound langugage
>> definition.
>
> I doubt that anybody outside academics really need and want this.
?
Just one example:
http://www.secunet.com/en/products-services/high-security/sina/sina-box/
They use two different tool sets for formal verification.
(Another example:
Some big money oil companies seem to be needing "deep see
electronics". Very small computers that need to be highly
redundant, robust, tolerant to fluctuations in power supply,
and other things as well. Things you find in OOSC2.
The makers say that they really needed to know what the
software would do because lives are at stake as well as very
large amounts of money. So you can't write software
be debugging it into existence. They started with MISRA C
but have recently switched to a no-no language that is
made with proofs in mind.)
Not surprisingly, RavenSPARK shares a number of limitations
with the SCOOP support recently announced. The SPARK
company does have customers, and these either sell software
or build software into their apparatuses.
Perhaps not surprisingly either, Helmut's language design
shares a number of things with an older no-no language that
has recently got "aspects" that can be attached to
declarations. These include, in particular,
preconditions of features,
postconditions of features,
type invariants (of expanded types, so to speak),
class-wide type invariants (of ref things, so to speak)
The no-no language (ISO standardized and commercially viable)
is a language with nesting that has many but not all of Helmut's
language's features, and a few more; in particular you cannot
pass closures up the call chain.
In further developing the no-no language, they use incremental
language design where possible (not always). Thus, preconditions
could to be written
pragma Precondition (boolean expression);
One goal was to see how (a) the new features could be implemented
and (b) how they would interact with other features of the
languages, such as inheritance or active multitasking types,
passive shared variable types, or generics.
But there are limits to this way of designing things,
I think that's for sure.
llothar
> software would do because lives are at stake as well as very
> large amounts of money. So you can't write software
Yeah sure and thats why they will trust a compiler and runtime with
such a small community. Come on any manager get a head shoot if he
really ever choose to do so.
Get real nerds - this crazyness of formal methods as the base language
foundation killed Eiffel. You can do formal methods on Java,C and
other crap languages too. But they are widely used so you can trust
the tools.
By the way, with dynamic memory management there is never a formal
verification. THis hasn't changed since i learned it in university.
Nobody needs a new buggy language to do security relevant stuff.
But a new modern language that creates fast and small programs - thats
where a demand is which was SmallEiffels domain.
Georg Bauhaus
>> The makers say that they really needed to know what the
>> software would do because lives are at stake as well as very
>> large amounts of money. So you can't write software
>
> Yeah sure and thats why they will trust a compiler and runtime with
> such a small community. Come on any manager get a head shoot if he
> really ever choose to do so.
The compilers, note the plural, have been around for two
dozen years or more.
Users trust object code review and related results when
that's required.
And the management wasn't shot; they do not manage by acting
like "everyone else" and they are supposed to do so AFAICT.
You seem to be saying that "much used" means "trustworthy".
A funny claim as it is contradicting the facts:
See bug databases for trustworthy tools. See the followup
problems of that most trusted, widespread systems programming
language's non-DbC int type creeping into so many other
languages; every other week yet another one causes a hole in
millions of program installations.
Similarly, "used by only a few" does not mean "can be trusted",
but the few may have built something the right way.
The right way is determined by the technical qualities of the
outcome, not by some perception of what is trustworthy and/or
how it relates to mass usage.
If modifying Eiffel means a way towards showing that an Eiffel
component (i.e. class) behaves correctly in all cases, i.e. if
showing correctness at the module level becomes easy, that's
a start.
> By the way, with dynamic memory management there is never a formal
> verification. THis hasn't changed since i learned it in university.
Not everyone seems to agree that dynamic means cannot be
verified. Just checking:
"Formal Verification of Industrial Software with Dynamic Memory
Management"
http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5703230
> Nobody needs a new buggy language to do security relevant stuff.
Who says new language? At least I didn't. The ones in question are
fairly old and well tested and have some troublesome parts removed
in their high integrity editions.
> But a new modern language that creates fast and small programs - thats
> where a demand is which was SmallEiffels domain.
Sequential programs? Yes.
Make SmallEiffel for Arduino providing add-ons that everyone will
like and see if that works.
OTOH, small as a goal? Not everywhere. Office Desktop means .NET,
server means JVM or similar.
A generator that translates Eiffel to Objective-C might be
interesting when, in a sense, this process adds DbC to Objective-C
as better input to Apple's static analyzers.
Helmut
>
> And again command-query separation and mulitthreading does not work
> together very well.
Oh yes, in concurrency you need command query separation more than in
sequential programming. But it needs to be adapted. More stricter
rules are necessary. That is one of the weaknesses of the current ISE
scoop concept.
>
> By the way: I like many of the features of modern Eiffel, one missing
> is to modernize the exception handling. A try catch finally style
> should be used.
Modern Eiffel has a better exception handling than ise eiffel. It will
have an exception handling that works well with concurrency. I agree
that exception handling should work also on a block level, not just on
the procedure level. If you read my draft description of Modern
Eiffel, you see that it has already a lot of "scoped" constructs where
ise eiffel has only "procedure" constructs. "Scoped" exception
handling fits in well.