12
$\begingroup$

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which strives to answer the question of "computability" i.e., things that can/cannot be computed with various constraints, I'm struggling to find the analog for "Theory of Programming"

Wikipedia describes it as:

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features.

This is like saying "everything" which isn't really specific.

The common progression of the topics is usually like so:

Combinatory Logic > Lambda Calculus > Martin Lof Type Theory > Typed Lambda Calculus > (Something happens here) > Programming languages developed - that have very little connection with CL/$\lambda$

I can see the underlying "math" involved with CL/$\lambda$ and interesting proofs that come out as a result including the Church-Rosser theorem and that's neat. However, I'm struggling to understand the "end goal" of all this undertaking? What's the holy grail of PLT if you will? For now it seems to just be scratching an intellectual itch but I can't really cross the bridge from research/theory to anything practical.

Note: I do get it up until using the $\lambda$-calc for undecidability proofs. But beyond its applicability to "computability" I just don't get it and am having a hard time even understanding the need for research in PLT from this narrow POV. Any existing books, references that can throw light on the "big picture" of PLT?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Your're totally ignoring whole swaths of PLT in your "common progression". For some reason your view seems to be skewed by $\lambda$-calculus and type theory. Let us have a look at the POPL 2019 accepted papers: concurrent randomized programming, probabilistic programming, verifiable assembly, algebraic effects, certifying neural networks, PL and hardware weak-memory models, quantum programming, etc. Lots of things which are not "just type theory", wouldn't you say? $\endgroup$
    – Andrej Bauer
    Apr 17, 2019 at 13:53
  • $\begingroup$ You're 100% correct. Hence I called out my "narrow POV". I am familiar with the "other topics" only by reading around here and checking out SIGPLAN/POPL Proceedings. I'm yet to find a "holistic reference/book" that gives a broad brush overview of PLT that includes the topics you mentioned. The type-theory bit is only from "my" POV of (creating?) programming languages. Would you have some pointers that could provide high-level introductions to the various areas of PLTto get a big picture overview? I'm curious to know what underlying "models" do they use and how? $\lambda$ everywhere? $\endgroup$
    – PhD
    Apr 17, 2019 at 18:04
  • 2
    $\begingroup$ @PhD There is no high-level introductions to the various areas of PLT that you want, c'est la vie! Maybe one day this will change. But don't hold your breath. The field is evolving fast, and differentiating itself into subfields. Other popular simple models include $\pi$-calculus, structural operational semantics, simple imperative calculi (like the WHILE language) and numerous others. Often one invents a toy calculus to suit one's application domain. $\endgroup$
    – Martin Berger
    Apr 18, 2019 at 13:27

1 Answer 1

Reset to default
17
$\begingroup$

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and associated tooling ecosystem.

Some reasons why maths is involved:

  • PLs are highly non-trivial, and it's not clear that they do the right thing without proof. The maths gives a simplified model of real programming languages. This model lets us study real programming languages in a much simplified setting, removing (hopefully) most problems already at the model level. Real programming languages are currently mathematically intractable. In other words: lambda-calculus is the fruit-fly, the E.Coli, the spherical cow of PLT.

  • PLT lacks suitable empirical methods, which would be nice / better to have, so maths is done as a substitute.

  • The maths is beautiful and deep.

  • The maths gives a simple, tried and tests research methodology, which is important for helping one's PhD students graduate. Typically, some variant of e.g.: Investigate PL feature XYZ through adding it to lambda-calculus. Add simple types for XYZ and prove type-soundness. Add generics for XYZ and prove type-soundness. Prove a parametricity theorem for XYZ generics. Add dependent types for XYZ and prove type-soundness. Develop a partial type-inference for XYZ dependent types. Add gradual types for XYZ and prove type-soundness. Add contracts for XYZ. Each of those is a paper. You can stop if your PhD student or postdoc runs out of time. Each of the above is interesting and will yield insight about generics, parametricity, type inference etc. This pipeline is a great way of navigating the difficult waters of all possible programming languages. A second way of learning is implementing languages in a compiler, but that's less tractable for an individual.

Whether PLT is needed is an interesting question. Most working programmers seem to think it's not. They are wrong: most languages developed by working programmers without a PLT background (e.g. Javascript, PHP) start out terrible, and make all the mistakes that PL theorists long learned how to avoid. If a PL developed by an amateur hits the mainstream, PL theorists need a decade or so fixing the obvious flaws (e.g retrofitting a static typing system, see Typescript). Let me summarise this situation:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

Aside: This state of affairs is entirely the fault of PLT because because most of them have no industrial programming experience, so don't really know what the pain points of working software engineers are. In particular, for sociological reasons, most PL theorists think that pure functional programming in languages like Agda is the solution to all problems, which does not stand up to scrutiny.

Improve this answer
$\endgroup$
20
  • 1
    $\begingroup$ @MartinBerger: Does CompCert count as an example of being able to handle a real-world programming language "theoretically"? If not, how high are you setting the bar, because CompCert is pretty impressive. $\endgroup$
    – Andrej Bauer
    Apr 17, 2019 at 13:40
  • 2
    $\begingroup$ @MartinBerger: Please consider watering down "most PL theorists think that pure functional programming in languages like Agda is the solution to all problems" because that's just your ranting and venting. For starters, even if you look at the topics that are currently present at ICFP and POPL, the majority is about impure programming languages. $\endgroup$
    – Andrej Bauer
    Apr 17, 2019 at 13:42
  • 5
    $\begingroup$ @PhD: there is a lot more to PLT than type theory. It's just that type theory is the first thing that you notice because it is one of the main tools of PLT. $\endgroup$
    – Andrej Bauer
    Apr 17, 2019 at 13:43
  • 1
    $\begingroup$ @AndrejBauer CompCert, CakeML etc are impressive, but they are far away from widely used compilers like LLVM, GCC etc. Moreover, compilers, unlike just about any real world software, do have a (kind-of / sort-of) specification, which you just don't get in normal industrial software engineering. Not to mention that a great part of Xavier's early work on CompCert consisted of precisifying the specification. $\endgroup$
    – Martin Berger
    Apr 18, 2019 at 8:46
  • 2
    $\begingroup$ @PhD Regarding ""radically more productive" than > non-PLT C/C++, Java, C#", please bear in mind that if you look at those languages, more specifically, their evolution over time, almost everything they've acquired over time, e.g. lambdas, monads (LINQ), pattern matching, partial type inference comes from PLT. The C# team has PLT PhDs. Indeed they tried to hire me at some point. The job interview was me trying to convince Anders Heijlsberg that C# needs generics, which he didn't like at the time ... $\endgroup$
    – Martin Berger
    Apr 18, 2019 at 8:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.