Explore to Exploit

Teach basic coding

We were thinking of How to Design Programs (HtDP) as a potential basis for this work. We would want to respect category theoretic concepts in the presentation.

There are analogues in settings like Bayesian modelling.

We could look at relationships with argumentation theory, thinking about how to do this in a theoretically consistent way. Once we have a definition of the programming language we’re going to use, we can then do argumentation over that.

Could we have a DSL for HtDP ideas, then we could reuse it to generate patterns for learning how to design some other structure (say, web pages or probabilistic programs).

To do this well you’d need ways to express ‘recipes’. For example, an MVP might be based on representing HtDP-style recipes using sequent calculi for session types. These represent interactive protocols.

You’d use cut-elimination to have two players interact (using something like the Lakatos Game diagram). But what formalism would you use? E.g., geometry of interaction in linear logic has been used for this kind of thing, but could it be used here?

Contributes to