@john-bernier Hi John, welcome to the forum! Can you tell us which specific topics at the interface of topos theory and computer science you plan to address?  

I think topos theory's basic correctness comes from the principle of locality. This means that reality is massively parallel and local, with multiple events happening all at once at the same time down to the quantum scale. The advancement of computer technology has forced us to face physical realities. Instead of making cores faster we can only make them in higher and higher quantities. The holy grail of the computing industry is now parallelism, which means making computers that better adapt to the principle of locality.

The problem is that all existing programming languages are based upon the idea of global time, not the pervasive reality of local time. This is unnatural. To partially solve this problem, computer scientists have developed the technology of automatic parallelism. This requires complex program analysis to determine how programs can be broken down into parts that run side by side. An example of this kind of automatic program analysis is Bernstein's conditions. This says that if we have two operations that write to separate memory areas and don't affect their respective inputs then we can perform automatic parallelization. The broader subject of dataflow analysis helps us to reason about computer programs in terms of their local effects.

It occurs to me that breaking up computer programs into parts needs algebraic semantics. The very word algebra means "the reunion of broken parts." A colleague recently informed me of the excellent text Algebraic Structure Theory of Sequential Machines (1966). This comes closer than any prior work I've seen to describing a local structure theory of machines, and it even approaches the formalism we need, but we can do better.

My recent work on studying information flows in the Sierpinski topos generalizes the previous model of Hartmanis and Stearns. The result is a dataflow model that is more powerful and elegant than any other I have seen. This convinces me that I am on the right track in using topos theory. Grothendieck studied the local properties of algebraic varieties using local ringed spaces. All I want to do is reason about the local properties of machines to achieve greater parallelism. That is the topic I hope to address.

@john-bernier Thanks for these explanations! I will look at your paper with interest. 

I am presuming you know about Steve Furber's work on the asynchronous ARM?

https://apt.cs.manchester.ac.uk/ftp/pub/apt/www/async/async_desc.html

@gavin-wraith Hi Gavin, welcome to the Forum! I am not familiar with that work by Furber; does it have any relation with toposes?

@ocaramello  No, not really. But I thought John Bernier ought to know about Furber, who led a team at Manchester University creating an asynchronous version of the ARM chip. 

I was seduced from mathematics to computing at a certain point in my career, a complicated story that is of little relevance here except that I may have influenced others. I had just discovered Pierre Curien's thesis on the Categorical Abstract Machine when Max Kelly invited me to Sydney in 1987, where I think I infected Bob Walters when I gave a seminar on it.

@gavin-wraith I agree with Steve Furber's basic premise in The Return of Asynchronous Logic. According to special relativity, there is no such thing as global time. Whenever we create a clock to make up our own artificial notion of global time comes with a cost. Asynchronous logic can help alleviate those costs.

This solves the problem at the source. However, we can't always do that, so there is a lingering need to build programs that work on stock hardware. This presents two possibilities: (1) automatic program parallelism achieved by compilers through program analysis and (2) manual program parallelism achieved using multi-threading.

Structure theory has implications for this kind of program parallelism. I presume you are familiar with the parallel map pattern. This pattern can be generalized to any computable function by product decompositions in the Sierpinski topos. Then the components of the product can be executed on separate threads. This is a typical application of the theory. However, it seems intuitive that the idea of local reasoning about computations should be a part of parallel computing practice. Topos theory can help us achieve that. I will have more to say about that in my next paper.