What needs to be done

I can't deal with any of the large issues in the world, but I think we can still make computing be the way it is supposed to be. That is the beauty of computers, you can mold them into any form you like. With that in mind, lets discuss what needs to be done to build the new future of computing.

Computation ought to be organized around the presheaf programming paradigm, instead of the functional or logical paradigms. Functions should be treated as much as possible as presheafs over the ordered pair category, while sets are presheafs over a single point. The presheaf programming paradigm will remove the ackwardness of the separation between functions and logic. In particular,

• We need classes for dealing with the different kinds of presheaves like quivers, higher order quivers, sets, functions, bijections, incidence functors, MSets, etc and a whole database of the most important algorithms on them.
• We need an extensive ontology of different classes of presheaves. Think something like graphclasses, but instead focusing on presheaves.
• We need tools like the copresheaf viewer that make it more pleasant to work with presheaves.
• We need to have a knowledge base of ways of using presheaves to deal with other branches of mathematics like ring theory, such as through the use of presheaf valued functors.
• We need to further develop the theory of the topos $Sets^{\to}$ and its use in the topos theoretic foundations of computation. In particular, we need research into more advanced mechanisms for modeling data dependencies using congruences in the topos $Sets^{\to}$.
• Finally, the more advanced applications of sheaves in algebraic geometry and logic should be implemented in the same system.

When you look at algebraic geometry, you see that the fundamental objects are sheaves and not sets. The logic used in algebraic geometry is a categorical logic and not a classical one. Set theory is obsolete.

The amazing thing which I have described in my research is that the fundamental objects of computation are also not sets but rather presheaves as well. Thusly, the same sort of objects are used in both algebraic geometry and in the topos theoretic model of computation. In short, to make computing more pleasant we need new technologies for dealing with presheaves.