[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Martin Rubey
Subject: Re: [Axiom-developer] Re: SPAD and Aldor again
Date: 17 Nov 2006 17:17:27 +0100
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.4

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 *.


> 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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]