Hi all !

I see a problem in the control of future J development. It is too
complicated for any single person or company to handle, as I see it. Yet
a lot of coordination is needed.

I think the solutions is to create a J algebra, something similar to
mathematics and logics, but executable. An executable proof system. I
think a program could be it's own executable combination of proof and
axioms.

The way to start, I think, is to build a language similar to J as a
system of axioms and identities, definitions built on these axioms and
other known identities. The language is as much as possible defined in
it's own terms. It's own proof. The number of axioms are minimized. We
then try to simplify. We complement the language definition with
identities between different language concepts.

The resulting algebra is then used as definition of the new, hopefully
J-like, language. The algebra can then be freely extended as long as the
axioms it is built on is not modified and the identities still hold.
Like mathematics and logics is freely extended today.

What i mean here is real mathematical and logical proof. If a and b are
integers and c is the mathematically correct result, we should get the
correct c for all values of a and b. Or we have to prove that, given the
a and b we have, we will always get the correct c.

I think the essence of what J is about is to create an executable
algebraic system, a parallel universe to mathematics, logics and
notations building on mathematics and logics. An executable algebraic
system in which we can prove that our programs will always give the
correct results.

Cheers,

Erling Hellenäs

----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm

Reply via email to