See comments below.
On 2017-08-08 12:09, Jack Andrews wrote:
too complicated for any single person or company to handle
jsoftware might disagree. but very few programs built over years of effort
are pure
to build a language similar to J as a system of axioms and identities,
why not just use J? it allows identities and axioms.
1. The problem was to control J development.
2. Because I want the identities to have mathematical/logical validity
and hold for all values of the inputs.
On 8 August 2017 at 17:27, Erling Hellenäs <erl...@erlinghellenas.se> wrote:
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
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm
