Functional - [ANNOUNCE] Anubis language 1.7 release

Author

[ANNOUNCE] Anubis language 1.7 release

David RENE

2006-06-02, 7:06 pm

Anubis developer team are happy to announce the release of version 1.7
of their language.

Anubis is a programming language which has been designed on the basis of
mathematical logic in order to avoid most usual programming errors.

Even if all sorts of errors cannot be avoided by Anubis, so many common
errors are detected by the compiler that the debugging time is reduced
by a factor of about 40 compared to languages like C C++ or Java.

Anubis is a functional language allowing imperative style and object
oriented style.

The Anubis compiler, by its extreme requirements, quickly puts the
programer into an advanced state of serenity. The sensation of safety
with respect to many types of programing faults makes the programing
more agreable, avoids the stress and eliminates the risk of regression
in case the program is reorganized.

You can discover Anubis and the formidable tricks induced by the Theory
of Categories on which it is based at http://www.anubis-language.com

Sincerely,
David RENE

Stefan Ram

2006-06-02, 7:06 pm

Stefan Ram

2006-06-02, 7:06 pm

ram@zedat.fu-berlin.de (Stefan Ram) writes:
> »If JavaScript is enabled in these applications, then the
> system is vulnerable to exploitation.«
>http://www.uscert.gov/current/curre...ivity.html#iis5

Sorry, the URI has become obsolete for this quotation.
This text now can be found on:

http://www.us-cert.gov/current/arch...01/archive.html

David Hopwood

2006-06-03, 7:02 pm

David RENE wrote:
> Anubis developer team are happy to announce the release of version 1.7
> of their language.
>
> Anubis is a programming language which has been designed on the basis of
> mathematical logic in order to avoid most usual programming errors.
>
> Even if all sorts of errors cannot be avoided by Anubis, so many common
> errors are detected by the compiler that the debugging time is reduced
> by a factor of about 40 compared to languages like C C++ or Java.

That's a very strong claim. Do you have any evidence for it?

I am skeptical, since in my experience at least 50% of debugging time is
typically spent on bugs relating to the high-level design of a system --
that is, the programmer correctly implemented an algorithm they intended,
but it turned out to be the wrong algorithm.

While language choice can potentially have some influence here (by allowing
the system to be implemented in a simpler way so that design errors are
more visible), it is difficult to believe that it could make a factor of
40 difference in overall debugging time. Especially not if we are comparing
it to languages like Java that are already memory safe and typesafe (mostly
statically typesafe, with a few dynamic checks).

> Anubis is a functional language allowing imperative style and object
> oriented style.

This is not uncommon: O'Caml, Oz, E, Common Lisp, Haskell, some would
say C++, all allow functional, imperative and object-oriented programming.
Apart from the basis in category theory (also an attribute of Haskell),
what differentiates Anubis from them?

> The Anubis compiler, by its extreme requirements, quickly puts the
> programer into an advanced state of serenity. The sensation of safety
> with respect to many types of programing faults makes the programing
> more agreable, avoids the stress and eliminates the risk of regression
> in case the program is reorganized.
>
> You can discover Anubis and the formidable tricks induced by the Theory
> of Categories on which it is based at http://www.anubis-language.com

I notice that the implementation is only licensed for non-commercial use.
An implementation of a new language cannot compete on this basis.

--
David Hopwood <david.nospam.hopwood@blueyonder.co.uk>

David RENE

2006-06-05, 7:07 pm

David Hopwood a écrit :
> David RENE wrote:
>
> That's a very strong claim. Do you have any evidence for it?

Actually, this is just the result of our experimentations since the year
2000.
Our team has written more than one million lines in Anubis, and we have just
noticed that we had very very less debugging than with languages like C.
I agree that the factor of 40 is an evaluation on the noze. Of course,
the comparison may be different when compared with higher level languages
like Caml or Haskell.

> I am skeptical, since in my experience at least 50% of debugging time is
> typically spent on bugs relating to the high-level design of a system --
> that is, the programmer correctly implemented an algorithm they intended,
> but it turned out to be the wrong algorithm.

Yes, you are speaking about what we call here 'intention errors' (as
opposed to 'formal errors'). You are right, this not really a problem of
language. This may be better seen as a problem of methodology, for
example related to how we define types. We have a small example of this
in our library, in the file 'library/examples/watt.anubis'.

> While language choice can potentially have some influence here (by allowing
> the system to be implemented in a simpler way so that design errors are
> more visible), it is difficult to believe that it could make a factor of
> 40 difference in overall debugging time. Especially not if we are comparing
> it to languages like Java that are already memory safe and typesafe (mostly
> statically typesafe, with a few dynamic checks).
>
>
> This is not uncommon: O'Caml, Oz, E, Common Lisp, Haskell, some would
> say C++, all allow functional, imperative and object-oriented programming.
> Apart from the basis in category theory (also an attribute of Haskell),
> what differentiates Anubis from them?

Anubis has been designed by someone who did not know Caml nor Haskell.
He was just inspired by Category Theory (and to a smaller extent by his
knowledge of Lisp). Hence, he did not try to be different. He just wanted
to realize his ideas. Now, a posteriori, we can still find some differences,
for example, it seems that how sums are treated in Caml and Haskell have not
much to do with the definition of sums in Category Theory, since pattern
matching and filtering does not reflect the fact that categorical sums are
actually 'disjoint' sums. In Anubis, the implementation reflects exactly the
categorical notion, essentially because of the design of conditionals.

Another point is that there is no notion of exception in Anubis. The
behavior
is always normal. This is partly due to then design of conditionals.

Another difference is the 'flavor' of Anubis, which is maybe a consequence
of the fact that the designer is a mathematician, not a computer scientist.
You like or you don't like, but it's sure that the syntax is quite
different.
The syntax of Anubis is of course essentially inspired by the usual notation
in mathematics.

>
> I notice that the implementation is only licensed for non-commercial use.
> An implementation of a new language cannot compete on this basis.

No, it's not true, because there exists three sorts of licences for
Anubis. It depends on what you intend to do with Anubis.

The first one is completly free for non-commercial use, and non-profit
organizations.
The second one is for small business such as a person wanting to make a
business alone without any company. (sale of shareware, etc...)
And the last one is for usual business, like industrialists, editors,
services companies, etc...
Of course the price is diferrent for each use.
We started this policy since a long time, and we have already users for
each sort of licence.
Because we are confident as for the qualities of our language, and how
much time you can save with Anubis, we propose these three sorts of
licence.
As for business companies, they want to have support, in other words
persons whom to speak to, hence we sell services among other things.

Sincerely

David RENE

Joachim Durchholz

2006-06-05, 7:07 pm

David RENE schrieb:
> David Hopwood a écrit :
>
> Our team has written more than one million lines in Anubis, and we have
> just
> noticed that we had very very less debugging than with languages like C.

Well, compared to C, I'd believe that any day.
C++ too - though a lot depends on how you use the language (I've been
told there are idioms that are very safe, so if people restrict
themselves to these, C++ can give you high programmer productivity, too).
With Java, I'm not so sure. It doesn't prevent bugs, but it's far better
at containing their effects and giving early alarms, so it's easier to
find the error.

> for example, it seems that how sums are treated in Caml and Haskell
> have not much to do with the definition of sums in Category Theory,
> since pattern matching and filtering does not reflect the fact that
> categorical sums are actually 'disjoint' sums. In Anubis, the
> implementation reflects exactly the categorical notion, essentially
> because of the design of conditionals.
>
> Another point is that there is no notion of exception in Anubis. The
> behavior is always normal. This is partly due to then design of
> conditionals.

Now *that* is interesting.

.... um, well, the *claim* is interesting.
What I actually found on the web page wasn't as interesting.
(Warning: I haven't looked too far into the details. The following are
first impressions that didn't look promising enough to warrant further
investigation; please correct me if I overlooked something relevant.)

Conditionals: Seems to be just normal pattern matching. It's restricted
to a single level (no provision for nested patterns), and it has a
slightly annoying restriction that patterns must be given in the same
orders as the cases of a sum type. There's also a simple exhaustiveness
constraint, though that's considerably weakened because you can cheat by
saying
if <expr> is <pattern> then <body> else <term>

No exceptions: Now how would Anubis handle non-total functions? E.g.
sqrt: real -> real
where the argument is negative?

> No, it's not true, because there exists three sorts of licences for
> Anubis. It depends on what you intend to do with Anubis.
>
> The first one is completly free for non-commercial use, and non-profit
> organizations.

That's the only one I found on the web site.
The other licenses should at least be mentioned.

But anyway...

Regards,
Jo

David RENE

2006-06-17, 8:20 am

Joachim Durchholz a écrit :
> David RENE schrieb:
>
> Well, compared to C, I'd believe that any day.
> C++ too - though a lot depends on how you use the language (I've been
> told there are idioms that are very safe, so if people restrict
> themselves to these, C++ can give you high programmer productivity, too).
> With Java, I'm not so sure. It doesn't prevent bugs, but it's far better
> at containing their effects and giving early alarms, so it's easier to
> find the error.
>
>
> Now *that* is interesting.
>
> ... um, well, the *claim* is interesting.
> What I actually found on the web page wasn't as interesting.
> (Warning: I haven't looked too far into the details. The following are
> first impressions that didn't look promising enough to warrant further
> investigation; please correct me if I overlooked something relevant.)
>
> Conditionals: Seems to be just normal pattern matching. It's restricted
> to a single level (no provision for nested patterns), and it has a
> slightly annoying restriction that patterns must be given in the same
> orders as the cases of a sum type. There's also a simple exhaustiveness
> constraint, though that's considerably weakened because you can cheat by
> saying
> if <expr> is <pattern> then <body> else <term>
>
> No exceptions: Now how would Anubis handle non-total functions? E.g.
> sqrt: real -> real
> where the argument is negative?
>
Because there is no notion of exception, a conditional *must* have some
treatement for *all* cases, even if some cases (actually all but a
selected one) are gathered into a default term: 'else <term>'.

The conditionals of Anubis are not pattern matching, because pattern
matching like in CAML for example, is performed through an ordered set
of filters, two of which eventually accepting the datum to be filtered.
This behavior reflects the fact that the sets defined by filters are not
necessarily disjoint. On the contrary, sums in category theory are
disjoint unions. When a datum belongs to such a sum, it belongs to one
and exactly one member of the sum. This is why conditional have exactly
one case per alternative, and heads of cases are not tried one after the
other, but a jump is performed directly to the right case. It seems that
pattern matching is inherited from Prolog (and maybe other systems), but
for sure not from an analysis of categorical sums. This is somewhat
theoretical, but in practice this means (among other things): no exception.

Nested 'patterns' (actually heads of cases in Anubis) could be possible
only in the case the second type has only one alternative (for the same
reason that all cases must be considered). The author did not implement
this feature, because he did not find it very useful. Furthermore, you
would have to unnest in the case you add an alternative to the second type.

Of course, all these constraints may seem to be boring, but after some
practice everyone finds that the global safety provided by Anubis is a
much more valuable feature than any set of syntactical shortcuts.

In Anubis the square root is of type Float -> Maybe(Float), where the
type schema Maybe is the same as in Haskell.

Of course, this means that 'exceptions' are treated in the way we type
the functions, not by some external mechanism. Even if this is
theoretically equivalent, in practice this makes important differences
in programming safety.

>
> That's the only one I found on the web site.
> The other licenses should at least be mentioned.

Yes, we will correct this in the future. But if you read the current
licence, you will notice that for commercial use, you must send a mail
to the Anubis team. The commercial licence is available on demand.

>
> But anyway...
>
> Regards,
> Jo

Best regards,
David

Joachim Durchholz

2006-06-17, 8:20 am

David RENE schrieb:
> Joachim Durchholz wrote:
> The conditionals of Anubis are not pattern matching, because pattern
> matching like in CAML for example, is performed through an ordered set
> of filters, two of which eventually accepting the datum to be filtered.

Hmm... I'm rather puzzled that you need *two* filters to accept
something in CAML. I'd have said there is one filter (the pattern) and a
result (the expression).
Would you care to explain what you mean when you say "filter"?

> This behavior reflects the fact that the sets defined by filters are not
> necessarily disjoint. On the contrary, sums in category theory are
> disjoint unions. When a datum belongs to such a sum, it belongs to one
> and exactly one member of the sum. This is why conditional have exactly
> one case per alternative, and heads of cases are not tried one after the
> other, but a jump is performed directly to the right case. It seems that
> pattern matching is inherited from Prolog (and maybe other systems), but
> for sure not from an analysis of categorical sums. This is somewhat
> theoretical, but in practice this means (among other things): no exception.

Sure.
I'm not 100% sure, but I think most FPLs have this kind of
exhaustiveness checking, too. Whether you get a warning or an error
depends on the language's specific design philosophy, I'd guess.

> Nested 'patterns' (actually heads of cases in Anubis) could be possible
> only in the case the second type has only one alternative (for the same
> reason that all cases must be considered).

Not really - if the language's design goal is to insist on exhausting
all possibilities, the programmer would simply have to enumerate all cases.

> The author did not implement
> this feature, because he did not find it very useful.

Sure. The Haskell and *ML folks thought otherwise.
Can't tell which variant is more useful in practice.

> Furthermore, you would have to unnest in the case you add an
> alternative to the second type.

A nested pattern would be something like

Pair (x, Pair (y, z))

No need to unnest here - this is a single-case pattern that deconstructs
a Pair of something and a Pair.

This might be useful in other ways. E.g. one could have the following
two guards:

Pair (x, Pair (y, y)) -> do something knowing that y = y
Pair (x, Pair (y, z)) -> do something knowing that y != z

(Here guard order matters.) (I'm not sure whether the above can be done
in Anubis at all, or whether it's too useful in practice. However, if
you have equality tests, then the above is useful, too...)

> In Anubis the square root is of type Float -> Maybe(Float), where the
> type schema Maybe is the same as in Haskell.

OK, that's a valid approach for square roots.

I don't think it's a valid approach in general.
You can't predict all potential problems and wrap them in a Maybe type.
There's always the odd bug, the slight oversight, or the outright idiocy
in the code, leading to "this can't happen" situations with inconsistent
data and/or unattained postconditions. The software must have *some* way
to abort the computation, and a higher layer must have *some* way to
recover from an aborted computation.
A purposefully simple exception mechanism would do exactly this.

Regards,
Jo

David RENE

2006-06-17, 8:20 am

Joachim Durchholz a écrit :
>
> Hmm... I'm rather puzzled that you need *two* filters to accept
> something in CAML. I'd have said there is one filter (the pattern) and a
> result (the expression).
> Would you care to explain what you mean when you say "filter"?
>
'filter' seems to be just the same as 'guard'. I did not say that you
need two filters to accept something, but that in principle two filters
*could* accept the same datum. This is why the order is important.
Consider your own example:

Pair (x, Pair (y, y)) -> do something knowing that y = y
Pair (x, Pair (y, z)) -> do something knowing that y != z

Something like Pair(1,Pair(2,2)) is able to pass through the first
filter but also through the second one (of course, this would happen
only if the first one is not present). This just means that the domains
(sets of expressions accepted by) defined by filters (guards) are not
disjoint. In this sens, it is impossible to consider pattern matching as
based on categorical sums which are necessarily disjoint. In an Anubis
conditional, after the test has been computed, a direct jump is
performed to the right case. We do not try to pass a guard, we know
which case is the right one and necessarily it will pass.

But there is another problem with your example. In the first line, you
don't know that the last two arguments are equal. You just know that
they unify. This is not the same as equal, at least mathematically. In
Anubis, expressions representing data are never unified, only types are
unified (This is needed because there are type parameters). From the
point of view of Anubis, heads of cases are not patterns. A datum will
never be blocked by a head of case, because again this not a guard. This
is just a declaration of the components of the datum.

>
> Sure.
> I'm not 100% sure, but I think most FPLs have this kind of
> exhaustiveness checking, too. Whether you get a warning or an error
> depends on the language's specific design philosophy, I'd guess.
>
Indeed, in CAML you get a warning when you miss a case corresponding to
an alternative in a sum type. In Anubis it is an error. This is needed
because there is no notion of exception. So, this fact which may seem
unimportant, is actually a basic consequence of the philosophy behind
Anubis. From the point of view of the designer of Anubis, it is very
important.

One basic principles of Anubis is 'no exception' regardless of
conditionals anyway, because Anubis has been designed by a
mathematician, and there is no notion of exception in mathematics. A
proof of a theorem (the analog of a program) is reliable precisely
because it takes all possible situations into account. Why should it not
be the same with computing ? In Anubis, (if you don't use 'alert' of
course, which is just a development tool similar to 'assert' in C) it is
warranted that the behavior is always normal.

>
> Not really - if the language's design goal is to insist on exhausting
> all possibilities, the programmer would simply have to enumerate all cases.
>
It would require to enumerate all cases of the second type within a head
of case of the first one. This is theoretically possible, but leads to a
complicated and difficult to understand syntax, again because Anubis
conditionals are not pattern matching.

>
> A nested pattern would be something like
>
> Pair (x, Pair (y, z))
>
> No need to unnest here - this is a single-case pattern that deconstructs
> a Pair of something and a Pair.

No, there may be a need to unnest, if the type whose unique constructor
is 'pair' receives a second constructor, for example, in Anubis, the
type defined as:

type P($T,$U):
pair($T head ,$U tail).

where $T and $U are type parameters (i.e. represent any two types),
could eventually be redefined as:

type P($T,$U):
pair($T head, $U tail),
leaf(String).

In this case, a datum of type P(?,?) is not necessarily a pair.

This has another effect in Anubis, which is that the compiler will not
define the destructors 'head' and 'tail' with the second definition
(albeit it does define them with the first definition), because with the
second definition , 'head' and 'tail' would be *partial* functions,
which is impossible in Anubis. If you want a partial function from T to
U, it must have type: T -> Maybe(U).

> This might be useful in other ways. E.g. one could have the following
> two guards:
>
> Pair (x, Pair (y, y)) -> do something knowing that y = y
> Pair (x, Pair (y, z)) -> do something knowing that y != z
>
> (Here guard order matters.) (I'm not sure whether the above can be done
> in Anubis at all, or whether it's too useful in practice.

In Anubis the above could be written like this (assuming that 'pair' is
the sole constructor of the type of the test):

if ... is pair(x,p) then if p is pair(y,z) then
if y=z
then do something knowing that y = z
else do something knowing that y != z

which is not much more complicated.

>
> I don't think it's a valid approach in general.
> You can't predict all potential problems

Precisely, the syntax and semantics of Anubis are designed in such a way
that we *avoid* all potential problems, so that there is no need to
predict them. In other words, data in Anubis are always consistent at
all stages of the computation (like in mathematics).

> and wrap them in a Maybe type.
> There's always the odd bug, the slight oversight, or the outright idiocy
> in the code, leading to "this can't happen" situations with inconsistent
> data and/or unattained postconditions. The software must have *some* way
> to abort the computation, and a higher layer must have *some* way to
> recover from an aborted computation.

Again, no, because this can never happen.

> A purposefully simple exception mechanism would do exactly this.

This is why Anubis has no need for such a mechanism.

Kind regards.

David

Marcin 'Qrczak' Kowalczyk

2006-06-17, 8:20 am

David RENE <david.rene@free.fr> writes:

> Of course, all these constraints may seem to be boring, but after some
> practice everyone finds that the global safety provided by Anubis is a
> much more valuable feature than any set of syntactical shortcuts.

I'm sceptic. Anyway, where can I find an example program written in
Anubis, as large as possible?

--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/

David RENE

2006-06-17, 8:20 am

Marcin 'Qrczak' Kowalczyk a écrit :
> David RENE <david.rene@free.fr> writes:
>
>
> I'm sceptic. Anyway, where can I find an example program written in
> Anubis, as large as possible?
>
Yes, I believe you, because every persons was sceptic like before
adopting Anubis language. You can find many examples of Anubis program
on Anubis distribution what you can download on the website
http://www.anubis-language.com
You can find interesting examples located in library/examples. But, all
of the libraries files are good too.

best regards

David

Joachim Durchholz

2006-06-17, 8:20 am

David RENE schrieb:
> Joachim Durchholz a écrit :
>
> Again, no, because this can never happen.

1) If there's choice in writing software, there is always the
possibility that something is wrong.
2) There are often many ways to check he validity of a result, not all
equivalent to the path that constructed it.
3) From (1) and (2) it follows that software can diagnose problems with
itself.

In other words, yes it can happen, regardless of software technology,
language design, or whatever else you might introduce to fight bugs.

You can eliminate classes of bugs, of course.
Introduce automatic garbage collection, and you eliminate
dangling-pointer bugs (but you keep resource leaks).
Introduce Algol-style static type systems, and you eliminate integers
misinterpreted as strings (but you keep the telefone numbers that make
it into customer name fields).
Build computer programs from specifications, and you eliminate bugs from
manual transformation to programs (but you keep the specification
errors, some of them still coding bugs).

In other words, designing a language on the pretext that there won't be
bugs is folly.

You may well have found ways to deal with a specific class of bugs.
What remains open to me is (a) what class this exactly is, (b) whether
it's very relevant in the first place, and (c) whether Anubis really
prevents them (or just squeezes them into another corner).

Sceptically yours,
Jo

Marcin 'Qrczak' Kowalczyk

2006-06-17, 8:20 am

David RENE <david.rene@free.fr> writes:

> Of course, all these constraints may seem to be boring, but after some
> practice everyone finds that the global safety provided by Anubis is a
> much more valuable feature than any set of syntactical shortcuts.
>
> In Anubis the square root is of type Float -> Maybe(Float), where the
> type schema Maybe is the same as in Haskell.

Speaking about safety: 10^10 seems to be equal to 1410065408 in Anubis
(I haven't installed it, just judging from library sources), and
average([10^9, 10^9, 10^9, 10^9]) is -73741824.

What is the point of guaranteeing that the computation doesn't fail
if the result is incorrect? I would prefer the computation to fail if
it's unable to compute the correct result. Of course it would be even
better if it computed the result; it's pathetic when a 21th century
language can't count past 2 billion.

--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/

Sponsored Links