People like to discuss about the history of Programming Language – just think about HOPL. In my passed three years, my learning and research is also most about the history, or the classical PL research, be it The Dragon Book, lambda calculus, linear type system, Hoare logic, or abstract interpretation.
However, in more recent months, I was thinking more about the future of Programming Language research.
Applying for PhD
The first incentive is my application to PhD programs. When composing my statement of purpose, I have to think: what do I want to work on in the next five years, and what is the possible topic on which I can produce good work. So it must be about future, and I’d like to share a segment of my SoP here:
- Can we provide programmers, even the average ones, with both safety and performance?
- Is it possible to close the loop of software construction, static analysis, testing and maintenance in a fully-automated, data-driven fashion?
- If we want to build certified infrastructure from scratch, where does the specification come from? How can we trust the specification itself?
- How to design a program language that provides security by construction?
They are not really mature anyway, and I would appreciate it a lot if you can work out one of them entirely (leaving the definition of entirety to your personal judgement).
However, you can see that my understanding of PL’s future was still limited to the software correctness & security aspects. But after that, I knew more, and got more motivated towards thinking about PL’s future.
Conferences & Interviews
In this period, I got more active in searching about question, and luckily, I can interact with many top researchers in this field through two conferences I attended (SPLASH 2016 and POPL 2017) and numerous interviews following my applications.
In SPLASH 2016, there is Onwards! 2016 co-located, and also some inspiring papers in the main OOPSLA track. In this year’s POPL, we also got a separate crazy OBT track, as well as nice POPL papers. BTW, there is also a full conference concentrating on more cutting-edge aspect of PL: SNAPL, I hope I can participate it someday.
I will try to select some of the futuristic papers in POPL and SPLASH here to give you a sense:
（I am not listing more fundamental contributions here NOT because they are not important for future – actually, a lot of foundational breakthroughs, like in SMT efficiency, are enablers of future. But we can’t quite see where people are moving from these more fundamental papers).
- A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
- Automatically Comparing Memory Consistency Models
- Beginner’s Luck: A Language for Property-Based Generators
- Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
- Component-Based Synthesis for Complex APIs
- Coupling proofs are probabilistic product programs
- Dijkstra Monads for Free
- Interactive Proofs in Higher-Order Concurrent Separation Logic
- LMS-Verify: Abstraction Without Regret for Verified Systems Programming
- LightDP: Towards Automating Differential Privacy Proofs
- Parallel Functional Arrays
- QWIRE: A Core Language for Quantum Circuits
- Relational Cost Analysis
- The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
- Towards Automatic Resource Bound Analysis for OCaml
- A Compiler for Throughput Optimization of Graph Algorithms on GPUs
- Accelerating Program Analyses by Cross-Program Training
- Asserting Reliable Convergence for Configuration Management Scripts
- Automated Reasoning for Web Page Layout
- Automatic Enforcement of Expressive Security Policies using Enclaves
- Chain: Tasks and Channels for Reliable Intermittent Programs
- Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided Transformations
- FIDEX: Filtering Spreadsheet Data using Examples
- Incremental Forest: A DSL for Efficiently Managing Filestores
- Probabilistic Model for Code with Decision Trees
- Purposes, Concepts, Misfits, and a Redesign of Git
- Ringer: Web Automation by Demonstration
- Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver
- Semantics-Based Program Verifiers for All Languages
- To Be Precise: Regression Aware Debugging
So, my understanding about PL’s future is pinned on several keywords (or buzzwords):
Distributed System, Meta-level Automation, Tools for Better Testing, Probabilistic Programming, SDN, Program Synthesis, Scalable Type System of Effects, Low-cost Formal Verification, Quantum Computing, Parallel Algorithms, Cost/Resource-sensitive Type System, Privacy and Security, GPU Programming, Data-driven Program Analysis, DSL
Also, during the interviews, I knew quite a lot of exciting new projects going on (except those appeared in the above listed ones):
- ExCAPE: “Synthesis for System Design”
- Petablox: declarative program analysis for Big Code
- VeriDrone: Foundational Verification of Cyber-physical Systems
- Polymorphic Blocks: Novel block-based UI for visualizing proofs and types
- ESpectro: security architecture for Node.js
- Proof Evolution: Using semantic information to patch proofs in Coq
- TPS: Temporal protein signaling pathway synthesis
- DNA Storage: Using synthetic DNA for hyper-dense archival storage.
- Incarnate: Programming Language Tools and Techniques for 3D Printing
- Puddle: A programming language for microfluidics
Summed up, I began to have an understanding of future’s PL research as
- More cross-disciplinary applications (Biology, Quantum, Security, CPS, Data Science, Machine Learning, etc.)
- Use new techniques (data-driven, solver-aided, probabilistic) in traditional problems
- Attack a new dimension of an old topic (resource/cost analysis, effect-guided compilation, property-based test generation)
Back to the Jungle
More recently, I began to work on some real world projects myself, and most of them are not directly relevant to my research interest. But I’ve also noticed the chances for applying the PL mindset onto a particular problem domain. I asked myself:
- Is there a more fit language/framework for low-level graphics programming? (esp. testing?)
- If we generalize PL as a Human-computer Interface, then how can we improve that, with newer hardwares such as VR headset?
- How to catch/prevent the mistakes in programming build script? How can we leverage DSL design, type system, or static analysis tools to do that? How would that improve the maintainability of the system?
It’s like – you are a PL researcher, but facing a very different, and very practical problems – will you see them differently from non-PL folks? How would that lead into a research problem?
Recap: Where are we going to from here?
Put in a larger context, I think PL research is about the methodology of problem solving using a machine. It doesn’t provide you with answer, but with tools (pure mental ones or concrete artifacts), to attack certain problems.
Like other System sub-fields, abstraction is at the heart of PL, though PL’s abstraction tends to be more formal and more general.
PL can be philosophically or mathematically founded, revealing the true nature of the language itself; Or, PL can be invented, engineered, and tuned for a wider audience. However, these two sides are not segregated, but linked through teaching and writing (so education and training is a very important, but often missing link).
“PL” is evolving. It is facing different models (multi-core, parallel, distributed, biological, quantum), applied in different problem domains (data-analysis, artificial intelligence, or even robotics), and having different concerns (security, complexity etc.). All of these require wild imagination, but the core principles of PL, as stated above, should still be respected in a deeper level.
I think good PL research in future will need tight collaboration between people with very different backgrounds. The PL process of structuring, reducing, and designing can be applied beyond traditional programming domain, towards any interfaces that
- Connect people with complex, artificial systems
- Helps people better control the system, understand the system, and use the system to solve hard problems
Let’s see how things will go.
- @yangsiran read this post and suggested that most of the paper here are more about “programming” compared to “languages”. And most of them are relevant to every life.
- @rainoftime suggested a reading: Research Summary of Prof. Mooly Sagiv. I found it quite eye-opening and it echoes with some perspectives in this blog post as well.