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

Reply via email to