... [snip] ...

I've been scratching at Wittgenstein, the Vienna Circle,
and Godel. It got me thinking about the notion of Type
hierarchies and the current view of Type theory, specifically
its use to eliminate paradox.

Which leads my thoughts to the current fad of types and
functional programming.

I think the whole notion of types and functional programming
eliminates the "interesting" part of computing. Specifically,
it attempts to eliminate self-reference and its most interesting
aspect of self-modification.

Systems that can't self-reference and self-modify are sterile.

I'm beginning to think that the key flaw in Godel's 2 theorems
is that they don't take self-reference and self-modification into
account. At this point it's just not clear to me how to express
self-reference and self-modification in Godel numbering.

... [snip] ...

Tim

On Wed, Apr 27, 2022 at 9:22 AM Tim Daly <axiom...@gmail.com> wrote:

> ... [snip] ...
>
> I guess that's where we differ. Axiom is a piece of research software.
>
> Axiom was never intended to be a product. IBM gave us two choices. Either
> find someone to market it (NAG) or throw it away. FOSS software did
> not exist at that time and we were not allowed to work on it in any
> capacity once it was sold. That stopped the research but not the desire.
>
> On the "little problem" front I have many things I would like to do with
> Axiom. For example, I have a hierarchical graph of about 50 different
> kinds of matrices arranged so Axiom's inheritence would fit perfectly.
> Within that set are things like unitary matrices which would have just
> the algorithms you need to do quantum computers. The DHMATRIX
> domain would be usefully extended to drive the several robots I have
> in my office. Fourier and Laplace transform algorithms would be very
> useful for robot dynamics. Graphics algorithms should be extended
> to show Bode plots. The graphics world could be extended to do 3D solid
> models to use with my 3D printer. Quantum-safe encryption uses
> lattices which would fit well with skew matrix algorithms. There are
> a lot of "little problems" I wish I had time to work on.
>
> Richard Hamming (of Hamming distance fame) has a youtube video [0].
> He used to ask his Bell Labs colleagues "What are the fundamental
> problems in your area and why aren't you working on them?"
>
> So what are the "fundamental problems" of combining computers and math?
> Why aren't you working on them?
>
> I see two streams of computer mathematics. The computer algebra
> stream started in the 60s/70s and uses the "It works for me" approach.
> The proof stream started in the 90s and uses the "Lets prove my
> current theorem". The two streams have only James Davenport
> in common.
>
> "Computational Mathematics" would be a combination of both of these
> streams. Proofs would make Axiom less ad-hoc. Proven computer
> algebra algorithms would vastly expand proof assistants with trusted
> results.
>
> I view "Computational Mathematics", combining computer algebra
> and proofs as one of the "fundamental problems" of this era. The
> SANE version of Axiom is my attack on a fundamental problem.
>
> Axiom is the best research platform available to show both camps
> what is possible in future mathematics. Axiom showed the power that
> comes from using mathematics as a scaffold architecture guiding
> the organization. Grounding the group theory scaffold with proofs
> will make Axiom a much more solid structure for future mathematics.
>
> That said, my real motivation is that this research is fun.
> I am pretty sure nobody but me will ever care.
> I'm a "research rat" by nature.
>
> Tim
>
> [0] You and Your Research
> https://www.youtube.com/watch?v=a1zDuOPkMSw
>
>
>

Reply via email to