> 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. On 8 August 2017 at 17:27, Erling Hellenäs <[email protected]> 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
