Upcoming talks

** No seminars October 24--November 14 **

November 21 : Alex Lew

Probabilistic modeling and inference are central tools in multiple fields, including artificial intelligence, statistics, and robotics, but can be tricky for practitioners to apply correctly. To make these techniques more accessible, probabilistic programming languages give users a formal language for expressing probabilistic models, and automate tedious and error-prone aspects of implementing Bayesian inference algorithms. But how can we think formally about what these tools are doing, and whether their inference engines are implemented correctly? And when the default inference algorithms don’t converge quickly enough, how can users tailor inference to the problem at hand without invalidating correctness guarantees?

In this talk, I’ll introduce the core ideas behind probabilistic programming languages and motivate the need for a formal approach to understanding their semantics. I’ll present a brief sketch of the recently introduced category of quasi-Borel spaces [1], which has been used to validate the correctness of several general-purpose inference algorithms for probabilistic programs [2]. Finally, I’ll present a new extension to that work that allows programmers to customize the behavior of these inference algorithms on a per-model basis in a sound-by-construction manner, ensuring that the resulting inference algorithms are still correct.

[1] Chris Heunen, Ohad Kammar, Sam Staton and Hongseok Yang, A convenient cateogry for higher-order probability theory, Logic in Computer Science 2017.

[2] Ścibior, Adam, et al. "Denotational validation of higher-order Bayesian inference." Proceedings of the ACM on Programming Languages 2.POPL (2017): 60.

December 5 : Tai-Danae Bradley (CUNY)

2020

February 6: James Fairbanks (Georgia Tech)


Past talks

2018

February 15 : Brendan Fong
An overview of Coecke, Sadrzadeh, and Clark's Mathematical foundations for a compositional distributional model of meaning.

February 22 : David Spivak
Fuzzy simplicial sets I.

March 1 : David Spivak
Fuzzy simplicial sets II.

March 8 : Brendan Fong
An overview of McInnes and Healy's UMAP: Uniform manifold approximation and projection for dimension reduction.

March 29 : Brendan Fong
The equivalence of hypergraph categories and lax monoidal functors Cospan(FinSet) --> Set.

April 5 : Enrique Boroquez (UNAM)

The idea is to explore the concept "Point", to look at it from different perspectives and see the connections given by the Stone Duality and the Gelfand Duality. Starting from a topological perspective, a point as an element of a topological space, we'll see the correspondences with ultrafilters, global elements in the category of Stone Spaces, morphisms that have as codomain the initial algebra 2 and how this morphisms correspond to valuations of a language in classical logic. We'll then go to boolean valued models, see how the points there have a probabilistic behavior and see some interesting consequences given by doing the forcing method through principal ultrafilters vs non-principal ultrafilters.Then we'll see the equivalences given by the Gelfand Duality: global elements in the category of locally compact spaces, characters of commutative C* algebras, maximal ideals, pure states (as positive, normalized functionals) and irreducible representations.

April 12 : David Spivak

April 19 : Remy Tuyeras
How to do genetics with category theory I.

April 26 : David Spivak

May 10 : Remy Tuyeras
How to do genetics with category theory II: Recognition of biological mechanisms.

May 17 : Christoph Dorn (Oxford)

"Higher categories" are algebraic structures which generalise categories, in the same way that categories generalise sets. The theory of these structures is ubiquitous in many areas of application of category theory. In this talk, we will motivate higher structure from applications in logic, type theory and programming languages. Surprisingly, a formulation of higher categories which is amendable to computer implementation has been missing for decades — with homotopy type theory being a notable exception of the special case of “higher groupoids”. Starting from elementary observations about compositionality in higher dimensions, will sketch a combinatorial approach to higher categories that gives rise to a programming language which we call “Globular” and which comes with an elegant geometric model. We will see that programs in Globular can capture complex higher-dimensional geometric deformations, and learn how, for instance, they can capture higher homotopy groups of spheres and other interesting geometric facts.

May 24 : Tim Havel
(Slides)

System Dynamics is a moniker coined by Jay Forrester over 50 years ago at MIT, when computers were just beginning to be used to simulate the behaviors of complex models of social and economic processes. Today it has a substantial following in business schools, management consulting firms, and some multinational corporations, with the goal of teaching "Systems Thinking" to their respective stake holders (see "Business Dynamics" by John Sterman). While it has since branched out into more sophisticated agent-based and dynamic network models (see this short article), it was initially based on a diagrammatic language for nonlinear ODEs that continues to play a central role in its applications. This talk will introduce this language and give some examples, with the hope that the audience will discover some analogies, and new applications, for the categorical formalisms it has developed for modeling and analyzing systems in a broader sense.

May 31 : Brendan Fong
Causal theories: a categorical approach to Bayesian networks.

June 7 : David Spivak

June 14 : Remy Tuyeras
How to do genetics with category theory III.

June 21 : Brendan Fong

I'll talk about an algebraic setting (in particular, a category) in which supervised learning algorithms can be composed, and then explain how this articulates the structure underlying backpropagation on a neural network. More details here.

July 19 : David Spivak

Decomposition spaces are combinatorial objects that allow one to decompose maps in a natural (co-associative and co-unital) way. All categories are decomposition spaces, but not vice versa. Decomposition spaces form a category, called Decomp, where the maps preserve the decomposition structure. I'll discuss these ideas and recent work (joint with J. Kock) where we show that every slice category of Decomp is a topos. One of them is the topos I discussed recently: that of "discrete temporal type theory".

July 26 : David Spivak

Decomposition spaces are combinatorial objects that allow one to decompose maps in a natural (co-associative and co-unital) way. All categories are decomposition spaces, but not vice versa. Decomposition spaces form a category, called Decomp, where the maps preserve the decomposition structure. I'll discuss these ideas and recent work (joint with J. Kock) where we show that every slice category of Decomp is a topos. One of them is the topos I discussed recently: that of "discrete temporal type theory".

August 2 : Antwane Mason (Rensselaer Polytechnic Institute)

Formal verification is the process of proving that a system adheres to a specification of its intended behavior. Like programming languages, there exists a variety of specification languages, each suited to describing distinct types of behavior. Some systems may require a combination of specification types and reasoning strategies to verify the whole system. This scenario motivates the need for heterogeneous specification languages. In this talk, we shall explore Farrell et. al.'s 2017 paper entitled "Combining Event-B and CSP: An Institution Theoretic approach to Interoperability". We shall see how the authors use category theory to establish interoperability between two specification languages, Event-B and CSP, focusing particularly on how they develop semantic preserving translations between the two languages.

August 9 : David Spivak

In last week's seminar, we heard from Antwane Mason about Goguen and Burstall's notion of institution, which is a category-theoretic formalism used for software specification and verification. The definition is usually phrased in terms of a satisfaction relation between models and sentences of signatures, and a certain bivariant coherence condition on it.

In this talk I will discuss a few different category-theoretic perspectives on this notion, including from categorical database theory, posetal bifibrations, and topos theory. In the order "signatures, models, sentences, satisfaction", we can view

  • databases as an institution via "schemas, instances, embedded dependency constraints, satisfaction",
  • any posetal bifibration as an institution via: "base objects, fiber elements, fiber elements, ≤", and
  • toposes as an institution via "toposes, points, truth values, satisfaction".
Finally, I'll give an alternative, equivalent definition of institution in terms of fibrations and opfibrations.

August 16 : Brendan Fong

A simple tutorial on Kan extensions: their definition, relationship with (co)limits and adjoints, and some basic examples. There will be plenty of time for questions.

August 23 : David Spivak
An introduction to double categories

August 30 : Brendan Fong
2-categories and adjunctions

September 10 : David Spivak
Adjunctions and Mates

September 17 : Remy Tuyeras

In this talk, we will use the concepts of left Kan extension and monomorphism to describe Genome-wide association studies used in genetics. This will be the opportunity to review the concept of Kan extension and see its real world applications.

October 1 : Reuben Cohn-Gordon (Stanford)

In cooperative conversation, speakers tend to prefer informative utterances, and listeners assume the speaker is being informative in order to draw inferences. For instance, if you hear me say "John liked half of the concert", you infer that he did not like to other half, since as an informative speaker, I would then have said "John liked the concert", were that true. Bayesian models can be used to formalize these inferences.

I show that a model of an informative speaker (that says as much as is possible) can be defined as a right Galois connection (right adjoint between posets) to a literal listener, understood as a monotone function (functor between posets) from utterances to possible worlds. Dually, a pragmatic listener (that deduces that no more is meant that is said) is a left adjoint of a literal speaker, understood as a monotone function from possible worlds to utterances. While elementary, this points to a deeper category-theoretic formulation of Gricean pragmatics and more generally, cooperative games.

October 11 : Paolo Perrone (Max Planck Institute for Mathematics in the Sciences)

Monads are a categorical concept which can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of “evaluating an expression partially”: for example, “2+3” can be obtained as a partial evaluation of “2+2+1”, and conversely, we can view “2+2+1” as a partial decomposition of “2+3”. This construction can be given for all monads on a concrete category, and it is linked to a simplicial object called the bar construction, of which it gives an operational interpretation: the bar construction is a simplicial set, and its 1-cells are partial evaluations.

We study the properties of partial evaluations for general monads on concrete categories. We prove that whenever the multiplication of the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms.

For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables, which is used to define martingales. It follows that a martingale is equivalently described as a chain of partial decompositions.

This talk is part of a work in progress on a general operational interpretation of the bar construction.

This is joint work with Tobias Fritz.

October 15 : David Myers (Johns Hopkins University)

In order to make a model of some system, we have in mind the sort of things in that system we intend to model; we have an ontology of our model, and we hope the things in this ontology correspond to the things in the system. But coming up with such an ontology is more of an art than a science. A model's success is judged on its ability to predict, not how much it matches our intuitive ontology. What things do our best models actually model?

Can we find a "natural ontology" of a model, one that comes from the model itself and contains only the things the model is modelling? What is a thing, anyway? In this talk, we will look at a categorical approach to these problems using the yoga of behavior types.

October 29 : Lee Mondshein

How can category theory be productively applied to extend concepts and techniques of logic and linguistics, so as to elucidate the behavior of biological networks?

I will discuss some concrete initial steps, based upon current categorical constructs in logic and topology, and will explain the relevance of emerging semiotic ideas concerning meaning-making and meaning transformation in biological networks.

November 5 : Remy Tuyeras

Linkage disequilibrium is the existence of a non-random relationship between two loci in the genome. I will show how one can talk about this type of relationship using a certain type of pedigrads in the category of idempotent commutative monoids.

November 19 : Ed Wike
(Slides)

A first look at a software development effort to implement the causal theory methodology in Brendan Fong's masters thesis, "Causal Theories: A Categorical Perspective on Bayesian Networks" (presented by Brendan at a seminar in May). This talk, which includes a demo of the prototype version, will have a brief overview of causal modeling, the categorical framework for causal theory models, the Python software used, how the users can draw causal graphs with the program, and plans for ongoing development. We will discuss the applicability of the causal theory model program and the potential benefits of applying category theory to analytical modeling.

November 26 : David Spivak

Brendan and I have been developing a new categorical viewpoint—and graphical calculus for—regular logic. I've recently been thinking about how some of the surrounding ideas might apply to learning and adaptation via something I might call a "theory building" adjunction. Some of these ideas seem to connect to Reuben Cohn-Gordon's recent seminar talk on the "Gricean adjunction" from pragmatics.

The ideas I'll present are at an early stage in terms of maturity, and the goal of the talk is to be fun and pictorial. Still, I will certainly make connections to the underlying mathematical abstractions.

December 3 : Alex Kavvos (Wesleyan)

It is informally understood that the purpose of modal (i.e. unary) type constructors in programming calculi is to control the flow of information between types. I will introduce a number of such constructors that are useful for security-aware functional programming, i.e. for writing programs without accidental high-level leaks of information flow. Following that, I will prove that the well-typed programs in calculi of this sort preserve confidentiality and integrity by design, by using some categorical algebra and a few background ideas from topology. (This talk is based on arXiv:1809.07897.)

December 10 : Brendan Fong

I'll present some foundational ideas behind the work David and I have been doing on graphical regular logic. In particular, I'll give a number of characterisations of the notion of meet semilattice. The aim will be to not only give an understanding of meet semilattices, but to illustrate general categorical lessons about limits, adjunctions, and monoidal functors.

2019

January 31 : Jules Hedges (Oxford)

Open games are a foundation of non-cooperative game theory that is strongly compositional: all games are built from small pieces using sequential and parallel composition operators. They form the morphisms of a symmetric monoidal category, and string diagrams provide a useful and intuitive way of visualising them that is an alternative to the traditional extensive form. I will focus on the foundations, which involves a careful analysis of how observable and counterfactual information interact in a game. Time permitting I'll discuss a close connection with open learners, from the paper Backprop as Functor by Fong, Spivak and Tuyéras.

February 7 : Brendan Fong
An overview of Ellerman's Partition Logic.

February 14 : Brendan Fong

In this talk I'll introduce monads and their algebras, illustrating the concepts using the finite probability distribution monad. In particular, in addition to defining monads and algebras for monads, I'll talk about free algebras and the Kleisli category for a monad. Examples will include the power set monad, maybe monad, and the Giry monad. We'll see how the notion of a stochastic matrix or conditional probability distribution arises from this set up.

February 21 : Tobias Fritz (Perimeter Institute)

I will explain how monads often arise as Kan extensions of graded monads. For example, the set of lists over an alphabet is the disjoint union of the sets of lists of each length. I will then show how this leads to a construction of a probability monad similar to the Giry monad. The graded monad approach lets us replace the use of measure theory by the combinatorics of finite sets, and makes precise the idea that a probability measure is an idealized version of a finite sample.

Joint work with Paolo Perrone.

February 28 : Sam Tenka

Come hear about my favorite category, the category whose objects are convex sets and whose morphisms are affine maps. Among these objects are the simplices. Maps between simplices correspond to (finite-support) conditional probability distributions. In fact, this category has (co)limits, tensor, and hom, and we may interpret these concepts probabilistically, too! We will end by diagrammatically reasoning about independence and statistical sufficiency to show Fisher's and Basu's theorems. This theory is incomplete, so I'd love your feedback during and after the talk.

March 7 : Brendan Fong

The Yoneda lemma is a central result in category theory. Roughly speaking, it states that any object in a category is determined by its web of relationships (ie. its hom-sets) with other objects. In this talk I'll make this idea precise, and discuss what limits look like from this perspective.

March 21 : Rúnar Bjarnason (Unison Computing)

This talk is a very informal introduction to adjoint functors, particularly from the perspective of software development. I'll give lots of examples of adjunctions to help the audience develop a general feel for how they come up in programming and indeed in everyday life. A basic familiarity with category theory and functional programming is assumed.

March 28 : Anthony Bau

In this talk I'll discuss a Fong, et al.'s setting for composable learning algorithms (details here: https://arxiv.org/abs/1711.10455), and formalize the category of recurrent models on top of this framework. I'll then attempt and fail to equip this category with a trace, a notion that usually formalizes recursion in categories of computations. I'll discuss the obstructions to finding a trace, and speculate about what a traced category of learning algorithms might look like.

April 4 : Natalie Stewart

A PERT chart is a project management tool used to schedule, organize, and coordinate tasks within a project. The data of a PERT chart is a list of activities, together with their durations and dependencies on each other; the PERT chart formats this data as a certain duration-weighted graph. In this talk we'll discuss how these durations form a preorder R, which in fact has the structure of a quantale. This allows us to see PERT charts simply as R-enriched categories, and think about project scheduling in terms of categorical constructions.

This talk is based on the following n-Category Café post by Simon Willerton: https://golem.ph.utexas.edu/category/2013/03/project_planning_parallel_proc.html. No familiarity with enriched categories will be assumed.

April 11 : David Spivak

I'll discuss the mathematical specification of a graphical user interface for logical reasoning. I'll begin with a detective story, where we see this graphical reasoning in action. Then I'll briefly discuss the math—we've seen most of it before in this seminar—namely that of "ajax bifunctors from the monoidal bi-category of corelations to that of posets." With that out of the way, I'll talk more about the GUI and consider further examples of how such a tool could be used in practice, for fun and profit.
(slides)

May 2 : David Spivak

Abelian categories are "convenient places to calculate", e.g. to do homological algebra. One nice feature of abelian categories is that they are regular, meaning that each has a well-working calculus of relations. This calculus can be given a graphical formulation, with a "user interface" of wiring diagrams that we can specify mathematically.

I'll present abelian categories from this point of view, with the following compressed mathematical specification: a graphical abelian calculus is a bi-ajax po-functor P: LinRel-->Poset. Unpacking this, I'll explain that there is a graphical syntax of linear relations, which is a mild ("thin") extension of Sobocinski's graphical linear algebra. It forms a po-category LinRel, and functors from LinRel to the po-category of posets provide semantic content to this syntax: they tell us how we can "fill the shells". Any lax monoidal po-functor P: LinRel-->Poset whose laxators have both left and right adjoints gives rise to an abelian category, and all abelian categories (up to equivalence) arise in this way.

May 9 : Alberto Speranzon (Honeywell)

We describe a novel approach to mapping an unknown indoor environment based on sparse sampling of people paths with minimalist sensor data. The problem is inspired by mapping the geometry of a building floorplan via “uncooperative sensing” — using data from such as camera feeds and other tracking-capable sensors. Unique challenges include having no knowledge of sensor placement, coverage or parameters, thus making such sensors “uncooperative”. The methods we develop are, at first, topological, to build a combinatorial model with the appropriate topology. We focus the modeling and analysis assuming sensors being cameras: using statistical information based on how people are detected in various cameras field of views, we are able to develop a model that captures topological information about the unobservable space. Such a model is further augmented to include a weak form of geometric information, and optimization techniques are used to approximate domain geometry.

May 16 : Diego Roque

An introductory overview of the paper "Total maps of Turing Categories", by Cockett, Hofstra and Hrubes.

May 23 : David Spivak

Planning in autonomous systems is generally hierarchical. A goal is given to a higher-level planner, which decides on a sequence of actions that will accomplish it given the current conditions. Each of these actions is then handed off as a goal to some lower-level planner. To make dinner, we need to go to the store, get ingredients, bring them home, and cook, but going to the store requires choosing a route, and in turn, each step along the route is accomplished by choosing and executing a certain sequence of muscle movements.

We will think of planners as generalized Markov decision processes, where we replace the nondeterminism-and-reward aspect of an MDP by an arbitrary monad M on Set. These will be the objects of a category M-MDP, and we formalize "handing off high-level actions to lower-level planners" as morphisms. If M is monoidal, the result will be a symmetric monoidal category, the idea being that a team of bosses can issue commands to be executed by a team of performers.

May 30 : Mitchell Riley (Wesleyan)

Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general "optic" construction. After a crash-course in the (co)end calculus, we will define optics generally and see that we recover lenses, including the lens laws.

July 30 : Kenneth Harris (UCL)

Many learning algorithms have invariances: when their training data is transformed in certain ways, the function they learn transforms in a predictable manner. Here we formalize this notion using concepts from category theory. The invariances that a supervised learning algorithm possesses are formalized by categories of predictor and target spaces, whose morphisms represent the algorithm's invariances, and an index category whose morphisms represent permutations of the training examples. An invariant learning algorithm is a natural transformation between two functors from the product of these categories to the category of sets, representing training datasets and learned functions respectively. We illustrate the framework by characterizing and contrasting the invariances of linear regression and ridge regression.

August 8 : Gershom Bazerman (Awake Security)

I will describe the idempotent distributive lattice completion of a partially ordered set, and characterize it as a reflector in a subcategory of Pos which shares all objects but only contains a special class of morphisms. From there we will examine Dependency Structures with Choice, which are a way of reformulating the ideas behind the Event Structures used in models of concurrent semantics, including those of Petri nets. Reachable posets of DSCs, under the the distributive lattice completion, let us view dependency structures topologically, and provide an elegant logical interpretation of “covering” relations of dependencies. Time permitting, I can also sketch future work that makes use of induced homological structure as well. This project is jww Raymond Puzio.

August 15 : Daniel Rosiak (DePaul)

Tolerance relations are binary relations where just reflexivity and symmetry, but not transitivity, are assumed to hold. Forcing transitivity is obviously natural (and very useful) in many mathematical contexts, but there are a variety of interesting applications where imposing transitivity simply does not seem appropriate. The category of tolerance spaces (with tolerance-preserving functions) has monoidal closed structures, and I will mostly look closely at a few applications and examples displaying what it looks like to enrich over this category.

I may also look briefly at some connections to t-norms—in particular lattice-valued t-norms (lifting the set of truth-values in a fuzzy logic beyond the real interval [0,1])—and some properties of fuzzy tolerance, in the course of which I will touch on some broader interactions with generalized (Lawvere) metric spaces.

Finally, I will make a few connections between all this and sheaves, and possibly indicate some more general ideas on metrics on the category of sheaves.

August 22 : Brendan Fong

When manipulating data, it is often convenient only to read and write to part of a data structure, leaving the rest untouched or changed in some minimal compatible way. Optics provide a modular, composable, and increasingly popular method for structuring such manipulations. Examples of optics include lenses and prisms. Optics are heavily based on the categorical notion of profunctor. In this talk I'll introduce both profunctors and optics, and give some idea about how the categorical theory influences the practical design of data accessors.

August 29 : Ben Sherman

Many algorithms are specified on real numbers and then implemented with finite-precision arithmetic, with the result that the implementations do not soundly compute the results expected from their specifications. I will present a programming language MarshallB, which in contrast allows sound computation with continuous values. MarshallB types are generalized topological spaces, and functions are generalized continuous maps; the generalization is because MarshallB has higher-order functions but the category of topological spaces and continuous maps is not closed, so we instead use a category of presheaves over spaces, which is closed. These higher-order functions are useful! There are higher-order functions for logical quantification, for optimization, for integration, and for constructing real numbers via Dedekind cuts. In this talk, I’ll give a brief demonstration of MarshallB, I’ll review the interpretation of simply-typed lambda calculus into cartesian closed categories, and then we’ll look in particular at presheaves over spaces, focusing on some specific higher-order functions and how they work.

September 26 : Simon Cho (Michigan)

We construct a nerve functor parametrized by a choice of quantale, exhibiting both the Vietoris-Rips complex and the magnitude nerve as instances of this nerve for different choices of monoidal structure on the nonnegative reals. Furthermore, the difference between how persistent homology processes the Vietoris-Rips complex and how magnitude homology processes the magnitude nerve is cast as a choice of whether or not to "localize" the corresponding nerves in a precise sense. Lastly, we mention some application-oriented observations naturally suggested by the perspective mentioned above.

October 3 : David Spivak

In this talk, we'll discuss lenses, which have lately been showing up all over applied category theory: in the theory of functional programming, databases, hierarchical planning, open discrete dynamical systems, open economic games, and supervised learning. Lenses are somewhat peculiar-looking things, but at least they form a symmetric monoidal category, denoted Lens.

I hold the opinion that lenses should really be viewed within the larger, more geometrically-flavored category of bundles—objects in Lens are the trivial bundles—and that the reason lenses look peculiar is because the geometric aspect is obscured when we restrict to the special case.

To explain this, I'll show that Lens embeds into a larger symmetric monoidal category that provides geometric intuition, has better formal properties, and will likely be more familiar to mathematicians, e.g. to algebraic geometers. From this viewpoint, lenses become strongly related to that of polynomial functors, which show up in functional programming as "containers" and in database theory as "functorial data migration". I'll generalize further so that examples of lenses include continuous dynamical systems and a more principled (though still partial) solution to the view-update problem in database theory.

October 10 : Brendan Fong

Morphisms in a symmetric monoidal category can be depicted using string diagrams; this is a celebrated fact that underpins much of applied catgeory theory. It often happens, however, that one wishes to use special, additional icons in a string diagram language; more formally, this means every object is equipped with additional algebraic structure. For example, in a hypergraph category each object is equipped with a notion of wiring, or in a category with products each object has a diagonal map. In these cases, the minimal structure required for a nice string diagram language is a simple compatibility condition between the algebraic structures on each object and the monoidal product. If this condition holds, we say that the category supplies the structure.

In this talk I'll give some examples of supply, and outline a few theorems that show the compatibility condition is really what is necessary for nice diagrams. The material will form an accessible introduction to my paper with David of the above title.

October 17 : John Burnham (Sunshine Cybernetics)

The market has plenty of user-friendly programming languages like Python and JavaScript, efficient, resource-aware languages like Rust and C, and secure, mathematical proof languages like Agda and Coq, but it is almost impossible to find one with all those characteristics. In this talk, we'll highlight the design decisions behind Formality, an upcoming non-garbage-collected, parallel, accessible proof language that targets this sweet-spot by using insights from elementary affine logic, optimal reductions and interaction nets.