fmap

Slightly tongue in cheek, but the analogy to programming is this:

> "Almost everything most programmers do can be done both in x86 assembly and your favorite non-kooky programming language. Certain Powers That Be seem to have decided that x86 is the foundation of computer science. [...] Why does it matter?"

The problem is that it is difficult to translate results in a theory built in ZFC to other "architectures". In mathematics, the architectures in question are not different axiom systems, they are different branches of mathematics.

Let me give you an example. There is a large body of work on differential geometry with many useful constructions. Classical differential geometry works directly in a model where manifolds are certain subspaces of (countable products of) R^n. These constructions have been successfully imported into many different areas of mathematics. In most cases people just had to tweak the definitions slightly and adapt the proofs by keeping the basic strategy and changing all the details.

What is happening here is that the underlying ideas of differential geometry are not specific to this particular model.

When faced with such a concrete model, our first instinct should be to abstract from it and ask which assumptions are required. This is difficult in ZFC, because in the end you have to encode everything into sets. It's not possible to reason about "abstract datatypes" directly, without literally building a notion of logic (generalized algebraic theory) and models of it within ZFC. Even then, the existence of choice means that you usually have to exclude unwanted models of your theory.

Coming back to differential geometry: You can generalize a lot of it by working in a differentially cohesive (infinity-)topos. This is terribly indirect (in my opinion) and looses a lot of the intuitions. A topos is literally a model of a certain logic. Alternatively you can work directly in this logic (the "internal language" of the topos), where the differential geometric structure is available in the form of additional logical connectives. You are now talking in a language where it makes sense to talk about two points being "infinitesimally close" and where you can separate the topological from the infinitesimal structure.

At the same time you reap the benefits that there are many more models of differential cohesion than there are models of "R^n modeled in classical set theory". You can easily identify new applications, which might in turn suggest looking into different aspects of your theory. It's a virtuous cycle. :)

This approach is deeply unnatural when working in set theory or arithmetic. You have to encode everything into sets or numbers and then these sets or numbers become the thing you are studying.

> Everything in mathematics is divorced from reality.

Mathematics is an abstraction, but it is still useful for talking about concrete problems. Your mathematical assumptions can be either close or far away from your problem domain. Sometimes we introduce idealized objects, such as unbounded integers, in order to abstract further and simplify our reasoning.

These ideal objects can then either be "compiled away" in specific instances, or really do ignore corner cases which might invalidate your results.

For an example of the former, you can assume that there is an algebraically closed field containing a specific field, give an argument in terms of this closure and then translate this argument to one which does not construct the closure explicitly. The translation is mechanical and does not represent additional assumptions you made.

The second kind of ideal object is something like the real numbers applied to physics. We can think of a real number as an arbitrarily good approximate result. In practice we can only ever work with finite approximations. At the scales we are operating on the difference is usually not relevant, but there might, for example, be unstable equilibria in your solutions which are not physically realizable.

> Better by what definition?

Informally, better because it is "simpler". There are fewer corner cases to consider, theorems are more inclusive, constructions are more direct.

Formally, the theory has more models and is therefore more widely applicable. Theorems have fewer assumptions (but talk about a different and incompatible type of objects).

> The onus is on critics to do better. Dieudonne/Bourbaki made a valiant and elegant attempt even if they intentionally snubbed the needs of probability theory. And "better" will obviously be judged by the broader community.

Oh, sure, but that's not what I want to argue about.

I can tell you with certainty that classical measure theory is complicated by the interplay of excluded middle and the axiom of choice. This is a technical result. You can see this yourself in textbooks every time the author presents an intuitive "proof idea" which then has to be refined because of problems with the definitions. In alternative models, or in a metatheory with alternative assumptions, the simple proof idea usually works out fine.

> “I never really thought about it, but it doesn’t much affect my work day to day one way or the other”

In my experience, people won't come out and say it, but this seems to be what everyone is thinking. :)

The problem with this is that it is wrong.

Classical ZFC in particular is a very strong and specific set of assumptions* with a very tenuous link to any practical application. If you actually want to develop a useful bit of mathematics it makes sense to consider the "foundations" as a moving piece. It's a part of the design space for modeling your problem domain, not some god-given notion of truth.

You can translate between different logical theories by building a model of one in another, so it's not like you loose anything. But it's cooky to insist that we should start with ZFC of all things.

---

*) I mean that second-order ZFC has basically no non-trivial models, so there is no real way of extending ZFC to talk about domain specific aspects of your problems.

You're right. Classical measure theory lives in a model divorced from physical reality. You can show that all of the fancy counterexamples which necessitate the complicated constructions of measure theory are artificial (e.g., the characteristic function of a non-measurable set is uncomputable).

There are better approaches to measure theory which live in different "foundations". For example, you can build measure and probability theory based on the locale of valuations on a locale instead of a sigma-algebra on a topological space. You can do even better by starting in a constructive metatheory and adding some anti-classical assumptions which are modeled by all computable functions.

The reason we are teaching classical measure theory as the foundation of probability theory is historical and because there are no good expositions available for most alternative approaches. It is really not the most straightforward approach.

---

Before you accuse me of being overly negative: classical measure theory offers a consistent approach to probability theory which is well understood and for which carefully written textbooks are available. If you really need to go back to the definitions to derive something then you need to know at least one consistent set of definitions. So it is useful to teach measure theory, even if it is more complicated than it has to be...

I'm referring to the axiom that being godlike is a positive property. You can show that being godlike is a positive property iff god exists.

You may be right that it is common to dismiss arguments that invoke Gödel's theorem. I've been guilty of this myself. However, just like with quantum mechanics the reason is that there are just so many people who invoke Gödel's theorem without understanding it as a technical result.

I'm not talking about "pseudointellectuals" in this case, unlike with quantum mechanics. I'm talking about actual working mathematicians who use oblique references to Gödel to, e.g., dismiss formal methods or constructive logic as worthless.

This is extremely annoying, since Gödel's theorem's, as the article rightfully points out, are precise statements about formal systems. There's nothing mysterious about any of it. When someone invokes Gödel you can usually take it to mean "I don't want to engage with this topic further" and not as a serious argument.

> This is the man who "proved" God's existence with modal logic,

I'm pretty sure that was a joke. The final assumption he makes in this proof is logically equivalent to "god exists".

There is actually a neat way around this by using typed assembly language/proof carrying code. If you had a type preserving compiler down to machine code you could use a separate proof checker (which you presumably wrote by hand in machine code) to convince yourself that the resulting binary implements its spec. :)

The spec of a compiler is also relatively simple, so there isn't a lot of room for backdoors there.

It's not misleading in this case. It's used in practice.

You have to understand that CompCert's main competition in this space was an ancient version of GCC without any optimizations. This is mostly an issue of certification. CompCert got the same certification and is already a great improvement just by virtue of having a register allocator...

There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/). It's making progress, but these things take time. :)

Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it comes to "internalized" constructions. "Sketches of an Elephant" is a good example of a textbook that pretty much presents everything twice. Once in an ambient set theory and once internally.

What I meant specifically is work such as the following:

  Internal Universes in Models of Homotopy Type Theory - https://arxiv.org/abs/1801.07664

which explicitly works in an extensional type theory with some axioms to simplify and generalize a complicated model construction.

> For example is there a full, unrestricted formalisation of category theory in HoTT?

You can formalize category theory in HoTT as presented in the book. This has some advantages over a presentation in extensional type theory or set theory (being able to work up-to equivalence) and some disadvantages (universes in categories have to be constructed explicitly, since the ambient universe is not truncated). In my opinion, it's not the case that one is strictly superior - in the end it always depends on what you want to do.

> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification

I suspect that most bugs are introduced because programmers do not have a clear idea of what their code is supposed to do. There are simply too many levels to keep track of at the same time. E.g., in C you are manually keeping track of resource ownership and data representation at the low-level, while at the same time keeping the overarching architecture present in your head. The latter typically has several moving pieces (different threads, processes, machines) and keeping a clear picture of all possible interactions is a nightmare.

Formal specifications can help with this, by first specifying the full system and then deriving precise local (i.e. modular) specifications. In my experience, programming is typically easy once I have a problem broken down into isolated pieces with clear requirements. It's just that most systems are so large that getting to this point takes serious effort.

Here you run into a cultural problem. You need to convince people to put effort into something that they do not implicitly regard as valuable. It makes sense to me that people aren't using formal methods, unless there is very little friction when getting started.

> So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing?

Empirically, yes it is (see e.g. "Finding and understanding bugs in C compilers"). Testing can show the presence of bugs, proofs show the absence of (a class of) bugs. This is a worthwhile exercise, even if your model is not perfect.

This is not an all-or-nothing proposition. There are lightweight forms of formal specification and proofs which you are probably already using. One example are types. If your program is well-typed it might still crash with a division by zero or some other runtime error, but it will not crash because you tried to execute code at address 42 after you mixed up your integers and code pointers.

> All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic

What gave you this idea? It is frequently useful to work over different base logics to obtain models of non-classical logics. E.g., when you work in categorical logic you usually work over an intuitionistic logic which can then be interpreted in an arbitrary topos. This gives you the ability to internalize any constructions you do "on the outside".

There is a large community of mathematicians fixated on classical first-order logic, but this is just because of tradition. For models of classical first-order set theory it just doesn't make much of a difference. This is not true of "all formalizations of non-classical logic".

Elm is different to ML in that it is explicitly designed to be a pure language. Purity is important for the Elm architecture and allowing arbitrary side effects in your apps would break everything.

That said, you could add effects and a JavaScript FFI using monads or algebraic effects. You could also get rid of a lot of boilerplate in the Elm architecture using existential types. It's a safe bet that the Elm developers know this. But all of these extensions would make the language less approachable. I think one of the reasons why Elm is doing so well is because it's not Haskell. :)

That's amazing! Do you have any insight as to which structural properties make this problem simple?

The reason I was asking after tree-width is that control and dataflow graphs in structured programming languages usually have small tree-width (which gets added to the maximum number of overlapping patterns during instruction selection, more or less) and this leads to the fast heuristics used by the PBQP solvers in llvm and libfirm. It's been a few years since I looked into this though, so I'm probably a bit behind the state of the art. :)

Ok, my first reaction is that this is that it's really wonderful work - straightforward and with a big payoff at the end.

But this really begs the question: why hasn't this been done before? People have been throwing resources at machine learning for a decade now, and somehow nobody has thought to perform instruction selection before executing a model to optimize the kernels used?

What other low-hanging fruit is out there? Automatic partitioning of networks over several GPUs and CPUs? Such dynamic load balancing algorithms have been available in the HPC literature since there was HPC literature. Fusing multiple primitives to simpler kernels? That's what linear algebra libraries have been doing for decades. Optimizing internal data layout (although that seems to be part of this paper)? Optimizing scheduling decisions to minimize data movement?

---

Also since the author seems to be reading this thread: Have you tried measuring the tree-width of the instruction selection DAGs you generate for the PBQP problem? The heuristics for solving these problems in llvm are applicable to tree-width <= 2, but could be extended to, e.g., tree-width <= 4 without too much slowdown. I wonder if there is still an iota of performance to be gained here. :)

The article is underselling Erlang's meteoric success. "Adoption was slow during the first few years." - After 5 years there was an international conference devoted to Erlang, a global community around it and the language enjoyed commercial success from the beginning.

It just goes to show that Erlang fills a real niche that is ill served by most other programming languages. Programming distributed systems remains painful in 2018 - not because there aren't any theoretical solutions to make it easier, but because there are astonishingly few practical systems that offer built-in support. Erlang is such a practical system and if you didn't already look into the language it is well worth your time to pick it up. :)

He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift.

In general, you can do this exhaustive search with any "compact" type and there are a lot of compact types. In particular, the (total continuous) functions from a discrete (i.e. a type with decidable equality) into a compact type are compact. And as the article shows, the (total continuous) functions from a compact into a discrete type are discrete. Together with the observation that the type of natural numbers is discrete and that every finite type is compact and discrete already gives you infinitely many compact types to play with.

One caveat with this whole work (which goes back to Martin Escardo by the way) is that this doesn't work with general recursion. E.g. in a language with general recursion you can write a program

  kleene : (nat -> bool) -> bool

which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.

That was a poor choice of words. Models of lambda calculus are invariant under beta-eta conversion, which is what I meant by program equivalence, but which is not the same thing as contextual equivalence.

Thus you get a representation invariant under computation. This remains decidable when you consider only normalizing programs as in STLC or related subsystems.

Most examples I tried didn't work very well, but when it did work it was truly neat. The performance makes sense from a quick glance into the paper. The model represents programs as paths in the AST, which is not sufficient to reconstruct the semantics, but is a good "fingerprint" of a program for fuzzy retrieval tasks. That's the domain which the authors wanted to target.

I wonder if there is really so much low hanging fruit still lying around, or if everybody who tried injecting some more domain knowledge into tools like this had quietly failed.

For example, the obvious way of building a distributed representation of, e.g., the simply-typed lambda-calculus (STLC) is by building a model. There are four local constraints that the model has to satisfy and the payoff is a representation that is invariant under program equivalence.

There are some complexity theoretic reasons why this cannot really work all the time (conversion in STLC is nonelementary), but even something that works in simple cases would be more robust than a statistical fingerprint that gets confused by the names of local variables...

> it is common because academia loves OOP.

Absolutely not! I doubt that anybody was ever taught OOP in an academic PL course, unless it was really an "introduction to programming" course, or their professor was working on this topic at the moment. The meaning of a program in an object oriented language with imperative features and inheritance is not pretty.

There are aspects of object oriented programming that are useful for structuring programs (hidden state) and others which are a recipe for disaster (recursive types). This complexity is always swept under the carpet when teaching OOP. Classes/inheritance/objects are always taught via imperfect analogies, which should tell you everything you need to know about how "easy" OOP really is.

No, the reason it is taught so widely is purely practical. It's a popular paradigm and a lot of practical programming projects might need an OOP background.

---

Edit: Just to be clear, I'm not trying to say that OOP is bad per se.

The information hiding and namespacing aspects of objects are really useful, both in theory and in practice. It's just that I think that implementation inheritance is an imperfect way of facilitating code reuse and not something you should teach to new students...

This is a really wonderful paper. For several years now we have been teaching a seminar about functional programming every year, where students present functional pearls (for the most part). This paper has been a staple of the seminar and I never got tired of seeing it presented or explaining it to people.

There are two things that could be improved about the paper in my opinion, but they are minor. First, the proof of the formula for the next sibling in the Calkin-Wilf tree (Figure 3 in the paper) becomes much more obvious when you express x and x_0' in terms of y instead of expressing y and x_0' in terms of x. Second, the Stern-Brocot tree is a bit of a detour without any real payoff. It's just as easy to go from the traced gcd directly to the Calkin-Wilf tree.

The latter part is a bit of a shame, since there are plenty of things that could be said about the Stern-Brocot tree (see e.g. Concrete Mathematics by Graham, Knuth, and Patashnik), but then it would have to be moved to the end of the paper. The paper doesn't do this in order to have the nice closed form solution for the titular enumeration at the end instead...

> When possible errors are part of the function specification, on the other hand, we are almost OK.

This is the single best piece of advice in this article. The second thing you have to document is the postcondition in case of an error - what state is the program left in?

With both a normal and an error postcondition you can fully specify your program. Like the author, I'm convinced that most of the pain with error handling stems from programmers ignoring the consequences of an error. That's the reason why approaches that force you to deal with errors explicitly (Maybe a, Result e a, etc.) end up being more robust. Otherwise, a part of the program just ends up missing.

However, from a theoretical perspective, exceptions are superior. The reason is that the error postcondition really does represent a non-local exit. Just like an ordinary return statement, it should be implemented as one instead of forcing programmers to walk the stack by hand. The latter is both less efficient and more error prone. Additionally, resource management must be integrated with error handling anyway and exceptions provide a clean opportunity to connect the two. This is one of the things that C++ gets right.

> does "differentiation" have any applications in implementing more complete programming languages?

I'm not sure about implementing per se, but you can extend some notion of differentiation to richer programming languages: https://www.sciencedirect.com/science/article/pii/S030439750...

The differential of a term does give you some information about how a term behaves under reduction, so I guess the answer is "maybe" - sounds like a fun project to work on. :)

More generally, there are models of linear logic built on a notion of differentiation (mentioned in the same paper as above), which might translate to a compilation of linear lambda calculus/classical processes/pi calculus/etc.

These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.

I am not sure what the parent meant specifically, but yes, there is quite a lot of work on quantum physics and logic, with regular conferences (https://arxiv.org/html/1701.00242) and some truly fascinating models for intuitionistic logics (https://arxiv.org/abs/0909.3468).

Not being a physicist I have no idea whether this is "the way forward" for quantum physics or anything, but the results that I do understand are non-trivial so there seems to be something there...

Lie groups come up very naturally in synthetic differential geometry (SDG) (http://www.fuw.edu.pl/~kostecki/sdg.pdf). In fact, the main advantage of SDG over the classical formulation of differential geometry is that it can be developed in a largely coordinate free fashion and that you can talk natively about differential forms.

That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.

You have far more freedom in modeling intuitionistic logic than you think. :)

In this case, the point is that in a logic for cryptography, you would have a type "S" of "bit strings of arbitrary but unknown length" which is restricted in such a way that you cannot eliminate into discrete types (such as the natural numbers). In particular, there would be no way of proving "x != y" for x, y in S at all unless you assume that there was some function which established this.

One way to get a model for such a logic is to interpret types as (reflexive) graphs and functions as graph homomorphisms. The resulting category is a topos and hence gives you a model of type theory.

There is such a wealth of knowledge about building models for intuitionistic logic that it is difficult to say what can and cannot be done without a thorough literature review.

That's a nice way of introducing type state programming in an affine programming language!

In general though, type state programming would be even nicer in a linear language. For example, in the http server I could start writing a response without ever writing a body. Rust would happily accept this code, because Rust is always allowed to throw away resources.

An affine language controls the duplication of resources, while a linear language controls both duplication and destruction of resources. In a linear Rust, a data structure would have to implement Drop in order to be silently deleted and in the http server "HttpResponseWritingHeaders" should not implement Drop.

Let me just stress the first point, because that's exactly where Rust and C++ differ: C++ templates really are untyped. There is no way to check whether a template definition is correct. A C++ compiler has to first expand the templates ("complete monomorphisation") and then perform type checking. Any errors you get will be in terms of the template instantiations, not your original code.

Unlike C++, Rust has a type system for the full language. In particular, traits are type checked once and you get errors in terms of the code you wrote yourself. There are other compilers that use complete monomorphisation, such as the MLton compiler for Standard ML, where you don't hear horror stories about terrifying error messages because your code was checked before being specialized.

I want to stress that this is a terrible design decision in terms of usability, because it is incredibly attractive from an implementation perspective. Parametric types are a delicate issue in an imperative language and always end up rejecting some perfectly fine programs. Monomorphisation both eliminates this issue and potentially leads to more efficient code, but your type errors will suffer.

I could say more about this - there are more trade-offs involved - but actually working with template heave C++ code is a better argument than anything I could say.

...That said, the examples in the blog post actually don't use any complicated machinery, and the quality of the compiler errors just comes down to very good engineering on the part of the Rust development team. :)