Re: [Axiom-developer] Re: SPAD and Aldor again

[Martin Rubey]

Ralf Hemmecke <address@hidden> writes:

> I would very much like to be able to use any fancy character to denote the
> multiplication of a monoid (not just ASCII).

I strongly disagree on this point. Any character OK, i.e., defining some
operation to be infix or postfix, but please stay with ASCII. You know, not all
keyboards provide all symbols, and it's a pain to look for a certain symbol
when you're on a conference in Prag or China. And no, I don't want to remember
character codes. And no, I don't want to have to use a GUI, since I often work
through a modem.


I agree with

> That Monoid/AbeleanMonoid should be resolved. I want to be able to say that
> the positive integers are a Monoid wrt. + and wrt *.

and

> Of course it should also mean to have a way to specify the behaviour of
> algorithms in a formal way so that programs can be checked
> automatically. Proof checkers should, of course, also be written in that
> language.

However, I'm afraid, I don't have 27 years left. And, top issue on my priority
list are dependent types. As everybody knows meanwhile. I want to get rid of
that stupid ANY workaround in the series domains.

Martin