How Could One Unify CMU and MIT

I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams. This is about practical computing and the cost and feasibility of software development in general. Here is the problem:

We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Scheme which can be embedded in a host program in the form of a library that exports an API which can interpret code on behalf of the host. These are a far call from the completely `agnostic' algorithms described in pseudocode.

So now we have a nice theory of programming language design as taught by Pierce, Harper, Pfenning, Wadler et al and a way of thinking about engineering as taught by Abelson, Sussman et al at MIT, and these two things don't really connect! The closest idea I have seen to joining these two approaches together is the one described by John Baez and Mike Stay in Physics, Topology, Logic and Computation: A Rosetta Stone. See Process Maths and Frank Pfenning's Course on Linear Logic.

MIT ran a programming and category theory course in 2020:

The actual title was 18.S097: Programming with Categories. The way you do programming with categories is by thinking in category theoretic terms and writing code in Haskell to instantiate some of these abstract ideas.

Brendan Fong and David Spivak then went on to found The Topos Institute.

What I want people to be able to do is to combine algorithms together by composing languages.  For example, if I have a typesetting language then I would like to to be able to typeset diagrams using a constraint programming language and have them appear in the resulting output, and I would like that language to be usable in various contexts within the document, such as in tables or multi-column pages. This is something that any web browser has to be able to do, but only in a limited way. For an example of the kind of things the language should be able to express, see A Geometric Constraint Solver by William Bouma et al. In this case the reduction relation of the language would encode the solvers (there are many different solvers that need to be able to interact wherever logically possible). My question is not how or whether this can be done, it's where are the tools that allow us to talk about how languages and interpreters can be composed. It sometimes seems to me that people have given all this up and settled for LLM-based chatbots.  So what happens when you ask Claude to talk about this idea? I tried asking Google search AI to tell me whether there were any tools to convert grammars from BNF to railroad diagrams and it made such a mess of this that it was funny! All it came up with that was even remotely relevant was a link to The Fuzzing Book.

This talk was from 2004, and Jonathan Sobel went to work for Cisco, ...


27:42 What does a categorical compiler look like? See Bob Harper's Course on Principles of Programming Languages.

Subscribe to William Byrd.

I talked about this in August 2022 when I was living in Tecate, B.C. 


See David Jaz Maiers - Compositionality via 2-algebra and Matt Prewitt on Technology Ethics

Comments

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Tensor Fields and Simplicial Complexes

FUTO FUBS