On Getting Machines to do Stuff

We have all these machines, but they aren't doing the right stuff because of the hidden agenda: they were never meant to do stuff we needed them to do, they were meant to be ways for other people to use to get us to do stuff. See FUTO FUBS and the Everything App.

I was prompted to write this by Girard's question "What is a question?" and his remarks about a DVD player at 17:42 in Jean-Yves Girard - Lectures at IHP thematic trimester : Semantics of proofs and certified mathematics.  The example question he gives is how do you know that it is a DVD player? And the answer is that you put in a DVD and it asks you a question! 

It struck me the other day that the way most people think of programming is quite different to how I think of it. I think of it as composition of ideas in a bottom-up sense: I have some ideas and they're like Legos, so I have a box of all sorts of ideas and each time I learn a new one it goes in the box. Then when I am feeling creative I imagine what I could make by putting together some of the things in my box. Other people perhaps aren't so lucky, because they're not doing programming to be creative, rather they are doing it to achieve some specific end, usually to do with their employer's need to make more money. So they are not freely assembling ideas, rather they are given some conditions under which they have to find a way to make a program work. They call this synthesis.

23:08 An example of something, ... I think it's an example of just two different ways to say the same thing, and I wonder people don't just start with saying the thing, then let others decide what that means in particular circumstances. I think Dijkstra knew how to do this. See my Weather Report on August 8, 2022.

Subscribe to Strange Loop. 

Sometimes we discover that what we thought were different ideas are actually the same idea, like constraint solvers and type inference.

See also Tomas Petricek's Course: Write your own tiny programming system(s)! 

Subscribe to Tomas Petricek.

See Jean-Yves Girard - Lectures at IHP thematic trimester : Semantics of proofs and certified mathematics and Frank Pfenning's Course on Linear Logic. And for more on this strange confusion we seem to have between analytic and synthetic: About Logic - Analytic and Synthetic Mathematics.

That was four years ago and I still haven't found anyone who wants to talk about this, let alone do something with it. Programmers all to busy talking to AI chatbots to have time to do anything else. 

 

Here's an example of why I think top-down analysis is a good idea in programming. It allows you to abstract structures in a very efficient way. The Finset construction he does here (6:21) produces a canonical ordering and it is very closely connected with isomorphism classes of finite vector spaces, because that's the problem category theory was originally developed to explore. Now if you think that's just to do with physics then think again. Look at the slide of Girard's above, on the Analytic Space. Herbrand's idea of the principal unifier applies to the process of program evaluation and proof search. Constraint solvers can be interpreted as interpreters! (35:00) Tout sur la table, y compris la table. See How Could One Unify CMU and MIT. See also Girard on the Synthetic (26:47)

 

It took five years for the Google librarian to suggest this book.

 

Subscribe to Topos Institute.

This is how some people imagined the future. A grand enterprise. I felt the same about computation but one can only go on alone so far before it starts to look like a fantasy with no sound basis in reality.

Subscribe to Evolved Magazine.