Live Logic: I'm Still Looking for A Job

Dianna Cowan, a.k.a. Physics Girl, on programming. At 4 minutes 51 seconds, "Right now, think about what problem you have. I bet you can think of a program or app which can solve that problem." I can. But I can't write that program or app.

It goes back to the first post I made on this blog, about this project: https://code.google.com/archive/p/metaprogramming/:

The idea is simple: instead of writing actual programs, we write programs which write programs. But rather than trying to invent one general purpose meta-language, what we do is design a new programming language for each application. This allows us to abstract from all the tedious detail such as having to decide which particular programming language to use.

It also allows us to solve some hard problems such as the one Ken Thompson identifies in his Turing Award speech On Trusting Trust. This is because a meta-programmed system does not actually have any concrete representation in source code, so is not susceptible to any attack that is based on recognising the source code of the target system.

I wrote some more about it in this essay: Genesis, and a year later I tried to interest the GNU/Free Software community in it with this: GNU Thunder. Now I'm going to try again, by describing the same underlying thing in a way that I hope might interest the decentralise/indieWeb/dWeb people: see Lee Camp on Protests Everywhere.

This is a course called Computer Security 101:

... it's being held in Room 303:

This is from Polyadic Pi-Calculus: A Tutorial:

To see the relevance of Linear Logic and semantics of System-F, see Appendix B.3 on page 154 of Girard, Lafont & Taylor's "Proofs and Types" :

... and read Dijkstra's The T.H.E. Multiprogramming System and The Mathematics Behind The Banker's Algorithm. To an idea what sort of view a system programmer would have of the system as Dijkstra described it, see The T.H.E. Multiprogramming System Mk II. The programming language of higher-order polyadic Pi calculus provides concise ways to describe these abstractions over processes.

You may also find "Morpheus"s type system interesting: described in This tutorial, and the paper Principal Type Schemes for Functional Programs by Damas and Milner.

To see why we need to be much more careful about the distinction between truth and meaning, see this, from the introduction to The Definition of Standard ML, by Robin Milner, Mads Tofte, Robert Harper and David MacQueen, and it's about language design in very general terms.

The job of a language-definer is twofold. First – as we have already suggested – he must create a world of meanings appropriate for the language, and must find a way of saying what these meanings precisely are. Here, he meets a problem; notation of some kind must be used to denote and describe these meanings – but not a programming language notation, unless he is passing the buck and defining one programming language in terms of another. ...

... The second part of the definer’s job is to define evaluation precisely. This means that he must define at least what meaning, M, results from evaluating any phrase P of his language (though he need not explain exactly how the meaning results; that is he need not give the full detail of every computation). This part of his job must be formal to some extent, if only because the phrases P of his language are indeed formal objects. But there is another reason for formality. The task is complex and error-prone, and therefore demands a high level of explicit organisation (which is, largely, the meaning of ‘formality’); moreover, it will be used to specify an equally complex, error-prone and formal construction: an implementation. We shall now explain the keystone of our semantic method. First, we need a slight but important refinement. A phrase P is never evaluated in vacuo to a meaning M, but always against a background; this background – call it B – is itself a semantic object, being a distillation of the meanings preserved from evaluation of earlier phrases (typically variable declarations, procedure declarations, etc.). In fact evaluation is background-dependent – M depends upon B as well as upon P.

The keystone of the method, then, is a certain kind of assertion about evaluation; it takes the form

B |-- P ⇒ M

and may be pronounced: ‘Against the background B, the phrase P evaluates to the meaning M’. The formal purpose of this Definition is no more, and no less, than to decree exactly which assertions of this form are true. [their emphasis, not mine.]

The relevance to security is that it is by subverting the meanings of evaluations that any parts of the system can potentially become hostile agents. So what we are aiming to do by using metaprogramming in this way, is to define many different ways in which these meanings can be rendered independently of their concrete representation in any particular part of the system.

Welcome to The Matrix: