<p><strong>Deriving fast JIT compilers from interpreters.</strong> It has long been known, that, in principle, compilers can be derived
from interpreters in a mechanical way. This is a special case of
partial evaluation, sometimes called <em>Futamura projection</em> [1].  The
textbook [2] explains the state-of-the-art at the end of the 1990s.
The core problem is that it has been difficult to get compilers derived
by partial evaluation to match the performance of handwritten
compilers (<em>&quot;O, Partial Evaluator, Where Art Thou?&quot;</em> L. Augustsson, 2010).
In a parallel development, (tracing) JIT compilers emerged, their
convoluted development might have started with [3]. The core problem
with (tracing) JIT compilers is that they are complex, and
expensive to develop.</p>
<p>Over the last few years, the situation  changed.</p>
<ul>
<li><p>Meta-tracing was developed [4]
which turns an annotated interpreter into a tracing JIT compiler. This is the
basis of PyPy [5] which is widely used [9].</p>
</li>
<li><p>In a parallel development, Oracle's new approach to Java compilation, Graal/Truffle
[6, 7, 8], is based on partial evaluation, and indeed uses Futamura
projections to convert an interpreter into a compiler (Graal is a
conventional JIT and Truffle does the Futamura projection).  It has
been claimed that this is the first time that partial evaluation
Futamura projection has led to a performant compiler.</p>
</li>
</ul>
<p>There is clearly some family resemblance between meta-tracing and partial evaluation, but the exact relationship, the shared abstraction, is not fully understood.</p>
<hr />
<sub>
<p>[1] Y. Futamura, <em>Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler.</em></p>
<p>[2] J. Jones, C. K. Gormand, P. Sestoft, <em>Partial Evaluation and Automatic Program Generation.</em></p>
<p>[3] J. G. Mitchell, <em>The design and construction of flexible and efficient interactive programming systems.</em></p>
<p>[4] C. F. Bolz, A. Cuni, M. Fijalkowski, A. Rigo, <em>Tracing the Meta-Level: PyPy's Tracing JIT Compiler.</em></p>
<p>[5] <a href="https://www.pypy.org/" rel="noreferrer">https://www.pypy.org/</a></p>
<p>[6] T. Würthinger, C. Wimmer, C. Humer, A. Wöß, L. Stadler, C. Seaton, G. Duboscq, D. Simon, M. Grimmer, <em>Practical partial evaluation for high-performance dynamic language runtimes.</em> <a href="https://chrisseaton.com/truffleruby/pldi17-truffle/pldi17-truffle.pdf" rel="noreferrer">https://chrisseaton.com/truffleruby/pldi17-truffle/pldi17-truffle.pdf</a></p>
<p>[7] <a href="https://github.com/oracle/graal/tree/master" rel="noreferrer">https://github.com/oracle/graal/tree/master</a></p>
<p>[8] <a href="https://github.com/oracle/graal/tree/master/truffle" rel="noreferrer">https://github.com/oracle/graal/tree/master/truffle</a></p>
<p>[9] <a href="https://news.ycombinator.com/item?id=36940871" rel="noreferrer">https://news.ycombinator.com/item?id=36940871</a></p>
</sub>

CC BY-SA 4.0
2023-09-24T15:15:26.673Z
The first usable version of PyPy was released in 2007; paper [4] (link [here](https://dl.acm.org/doi/10.1145/1565824.1565827)) was published in 2009. For clarity, it would be better to talk about RPython, the toolkit which builds PyPy; this toolkit was isolated in the early 2010s and is now available as a standalone package for non-PyPy usage.
Corbin
CC BY-SA 4.0
2023-10-02T07:34:03.777Z
I recomend this book https://www.itu.dk/people/sestoft/pebook/
amirouche
CC BY-SA 4.0
2023-09-23T13:35:57.203Z
2023-09-23T15:06:31.303Z
2023-09-23T15:06:31.303Z
Martin Berger
<p><strong>Low precision floating point data types.</strong> Historically, most programming used the IEEE 754 Standard for
Floating-Point Arithmetic. Simplifying a great deal, IEEE 754 floats (64 bits version) give you</p>
<ul>
<li>Lot of precision (53 bits mantissa).</li>
<li>Small exponent: 11 bits.</li>
</ul>
<p>Historically, this was a good choice for many applications at the time. But it turns out that this was not good for deep learning. Simplifying a great deal:</p>
<ul>
<li><p>Needs lots of memory for each floating point number.</p>
</li>
<li><p>Small exponent is problematic, because during training we often
encounter extremely large or extremely small values.</p>
</li>
<li><p>High precision leads to overfitting, since high precision is a form
of model capacity Having low precision arithmetic can be seen as a
form of regularisation.</p>
</li>
<li><p>Maybe most important is the hardware perspecive:</p>
<ul>
<li>Multiplication of exponents uses <span class="math-container">$O(n)$</span>
transistors in the size of the exponent (multiplication of exponents is done by adding),</li>
<li>Multiplication of mantissa uses <span class="math-container">$O(n^2)$</span>
transistors in the size of the mantissa.</li>
</ul>
</li>
</ul>
<p>By using less precision (mantissa) but bigger exponents we need
fewer transistors per (floating point) arithmetic unit in processors,
so we can pack more arithmetic units into each processor, which
increases FP performance. This lead to experimentation and Google's first TPU uses
the  <code>bfloat16</code> floating-point format</p>
<ul>
<li>Sign bit: 1 bit</li>
<li>Exponent width: 8 bits</li>
<li>Mantissa: 7 bits</li>
<li>Different handling of underflows, overflows, and NaNs.</li>
</ul>
<p>This lead to a flurry of activity, and modern CPUs and GPUs all
provide for such low precision floating point numbers.</p>
<p>Given the preponderance of arithmetic units for low precision floating point arithmetic in modern processors, an interesting question is: how efficiently to bootstrap
high-precision floating point operations from low precision floats?</p>
<p>(Note: I'm not sure about the history of low precision floats, that's why I'm not adding references. Feel free to edit.)</p>

CC BY-SA 4.0
2023-09-24T12:26:12.940Z
I don't see how that's a CS advance. For as long as FP have existed you could have made them with larger exponents and smaller mantissas.
toasted_flakes
CC BY-SA 4.0
2023-09-24T13:30:20.113Z
@toasted_flakes You can simulate the new short floats, but that would be *much less* efficient than having them as hardware primitives, presumably orders of magnitude less (just think about memory usage of your scheme, or transistors that are needed for IEEE 754 float multiplication vis-a-vis bfloat16). So I don't think you can simulate using comparable memory and transistor budget. Also, we have empirical evidence about the effect of different float formats on deep learning. None of this existed until recently.
Martin Berger
CC BY-SA 4.0
2023-09-25T02:02:03.750Z
@toasted_flakes: I agree, it's not a new advance in computer **science**, it's just a case of different engineering tradeoffs for the same basic format becoming useful (and commercially relevant) for a new problem domain.  The "science" part of this is the observation that deep-learning still works fine with few mantissa bits, enabling us to make that different engineering choice for an already-known approach to representing real numbers with fixed bit width.
Peter Cordes
CC BY-SA 4.0
2023-09-25T02:04:23.747Z
@toasted_flakes: A *new* approach to representing real numbers is the Posit, which avoids spending coding space on NaNs and Inf, and has gradual *overflow* for more dynamic range in limited bits, vs. IEEE FP having gradual underflow (subnormals) but hard overflow to +Inf.  https://spectrum.ieee.org/floating-point-numbers-posits-processor / https://www.johndcook.com/blog/2018/04/11/anatomy-of-a-posit-number/   Posit support is even more limited in hardware that bfloat or IEEE FP16, but apparently Posit FPUs aren't too expensive to build.
Peter Cordes
CC BY-SA 4.0
2023-09-23T12:50:40.343Z
2023-09-24T13:26:56.400Z
2023-09-24T13:26:56.400Z
Martin Berger
<p><strong>Liquid types.</strong> Introduced in [1], and refined in multiple follow-up papers. Liquid types can be seen as a form of dependent types that break with
traditional type theory which is keen to
have 'nice' typing rules that can be seen logical rules (this is the Curry-Howard
perspective). Instead, liquid types are developed with a view towards maximising automation: all constraints during type-inference are simply
handed to an SMT-solver, and automatically solved.</p>
<p>Liquid types  are now used in industry for processor specification and
verification through the Sail language [2], which is widely used, most prominently, for specifying the RISC-V instruction
set architecture [3].  There are concerted efforts at augmenting
general purpose languages with liquid types, in particular</p>
<ul>
<li><p>Haskell [4]</p>
</li>
<li><p>Rust [5]</p>
</li>
</ul>
<p>and probably more that I am not aware of.</p>
<p><sub>(I used to be sceptical of using types much stronger than Damas-Hindley-Milner style <em>Let-Polymorphism</em> in general-purpose programming languages due to the loss of convenient type inference. Liquid types changed my mind.)</sub></p>
<hr />
<sub>
<ol>
<li><p>P. M. Rondon, M. Kawaguchi, R. Jhala, <em>Liquid Types.</em> <a href="https://goto.ucsd.edu/%7Erjhala/papers/liquid_types.html" rel="noreferrer">https://goto.ucsd.edu/~rjhala/papers/liquid_types.html</a></p>
</li>
<li><p>A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray,
M. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur,
I. Stark, N. Krishnaswami, P. Sewell, <em>ISA Semantics for ARMv8-A,
RISC-V, and CHERI-MIPS.</em> <a href="https://github.com/rems-project/sail" rel="noreferrer">https://github.com/rems-project/sail</a></p>
</li>
<li><p><a href="https://github.com/riscv/sail-riscv" rel="noreferrer">https://github.com/riscv/sail-riscv</a></p>
</li>
<li><p><a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="noreferrer">https://ucsd-progsys.github.io/liquidhaskell/</a></p>
</li>
<li><p>N. Lehmann, A. Geller, N. Vazou, R. Jhala, Flux: <em>Liquid Types for Rust.</em> <a href="https://github.com/flux-rs/flux" rel="noreferrer">https://github.com/flux-rs/flux</a></p>
</li>
</ol>
</sub>

CC BY-SA 4.0
2024-08-19T16:03:58.697Z
Do you know if/how this relates to [F*](https://fstar-lang.org/)? F* is all about dependent types and using an SMT solver, but I have no idea if that's the same or different approach.
cubuspl42
CC BY-SA 4.0
2024-08-20T03:09:48.353Z
@cubuspl42 Not in detail. Both F* liquid types are based on refinement types, but F*'s are more powerful, in that F* does *not* only support type-based reasoning about programs, unlike liquid types.
Martin Berger
CC BY-SA 4.0
2023-09-23T11:43:57.297Z
2023-09-23T15:29:40.710Z
2023-09-23T15:29:40.710Z
Martin Berger
<p><strong>Newer data structures</strong>. The mighty Bloom filter, which has been around since 1970, provides a way to store an approximation of a set of <span class="math-container">$n$</span> elements with false positive rate <span class="math-container">$\varepsilon$</span> using approximately <span class="math-container">$1.44 n \log_2 \varepsilon$</span> bits. In 2014 the cuckoo filter, based on cuckoo hashing, provided an alternative using approximately <span class="math-container">$1.08 n \log_2 \varepsilon + 3n$</span> bits while supporting deletions, while the 2019 <a href="https://stackoverflow.com/questions/67527507/what-is-an-xor-filter">XOR filter</a> supports the set in <span class="math-container">$1.23 n \log_2 \varepsilon$</span> bits. While a full analysis of cuckoo filters is still open as of 2023, the theoretical basis for XOR filters is decently well understood and the connection to hypergraph peeling and orientability led to further improvements (most famously the Ribbon filter, which has been used at scale at Meta).</p>
<p>In 2017 the zip tree was invented, providing a way to build a randomized balanced binary search tree using <span class="math-container">$O(\log \log n)$</span> random bits per element. The height of zip trees slightly exceeds that of treaps, but in 2023 the zip-zip tree was introduced, which matches the theoretical guarantees of treaps using only <span class="math-container">$O(\log \log n)$</span> bits of randomness per element. To the best of my knowledge this data structure isn’t used in practice, but it’s definitely worth a look.</p>
<p>Just missing your cutoff, in 2009 the SA-IS algorithm for building suffix arrays was introduced. It runs in time <span class="math-container">$O(n)$</span> and is quite fast in practice. One of the most widely used suffix array construction algorithm libraries (LibDivSufSort) is based on the techniques developed in this algorithm.</p>

CC BY-SA 4.0
2023-09-24T19:34:55.933Z
[Hollow heaps](https://arxiv.org/abs/1510.06535) (2015) are another example of a direct improvement over an existing data structure.
Challenger5
CC BY-SA 4.0
2023-09-25T01:27:42.963Z
I’ve heard of hollow heaps but wasn’t aware that they were an improvement over other data structures. Can you elaborate? (I teach a course on “advanced” data structures and am always looking to modernize the syllabus!)
templatetypedef
CC BY-SA 4.0
2023-09-26T05:26:03.233Z
Hollow heaps provide the same asymptotics as Fibonacci heaps, but improve the constant factors, which afaik are so high for the latter that it is never used in practice.
Challenger5
CC BY-SA 4.0
2023-09-24T01:30:25.660Z
2023-10-06T11:19:33.473Z
2023-10-06T11:19:33.473Z
templatetypedef
<p><strong>Translation validation of compilers.</strong>
In compilation, especially optimising compilation, correctness is a big issue for obvious reasons.
Ideally, we'd like the whole compiler being proven correct once and for all, but this is beyond the state-of-the-art in 2023 for
industrial strength compilers like LLVM  and GCC (still there is progress, see CompCert [1]
CakeML [2]).</p>
<p>However, we should not let the perfect be the enemy of the good: enter <em>translation validation</em> [3]. The idea is simple:
instead of giving a <strong>single</strong> proof that the compiler is correct for <strong>all</strong> input programs <span class="math-container">$P$</span>, we prove, for an individual program  <span class="math-container">$P$</span> that the translation of
<span class="math-container">$P$</span> is correct. This is much less demanding. Note that proving that the  compiler correctly translates a given program <span class="math-container">$P$</span>, does <em>not</em> imply that it
also translates other programs correctly! That may sound really weak, but, empirically, translation validation is useful [4, 5, 6]:</p>
<ul>
<li><p>Translation validation (at least of individual optimisation passes) can be automated with SMT solvers like Z3, even for complex LLVM optimisation passes.</p>
</li>
<li><p>Doing translation validation for a modest size number of programs finds huge number of bugs in complex LLVM   optimisation passes automatically</p>
</li>
</ul>
<p>This raises more questions: for example, is the translation validator itself correct?  See [7] for recent progress in this direction.</p>
<hr />
<sub>
<p>[1] X. Leroy, <em>Formal verification of a realistic compiler.</em> <a href="https://xavierleroy.org/publi/compcert-CACM.pdf" rel="noreferrer">https://xavierleroy.org/publi/compcert-CACM.pdf</a></p>
<p>[2] <a href="https://cakeml.org/" rel="noreferrer">https://cakeml.org/</a></p>
<p>[3] A. Pnueli, M. Siegel, E. Singerman, <em>Translation Validation.</em></p>
<p>[4] N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr, <em>Provably Correct Peephole Optimizations with Alive.</em></p>
<p>[5] N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, J. Regehr, <em>Alive2: Bounded Translation Validation for LLVM.</em></p>
<p>[6] <a href="https://github.com/AliveToolkit/alive2" rel="noreferrer">https://github.com/AliveToolkit/alive2</a></p>
<p>[7] J. Lee, C.-K. Hur, N. P. Lopes, <em>AliveInLean: A Verified LLVM Peephole Optimization Verifier.</em></p>
</sub>

CC BY-SA 4.0
2023-09-23T14:46:55.650Z
2023-09-23T15:12:48.687Z
2023-09-23T15:12:48.687Z
Martin Berger
<h3>async/await pattern</h3>
<p>I'm not really sure how well this fits the criteria (especially the &quot;since 2010&quot; part is kinda fuzzy here), but I myself consider this to be the most significant <strong>practical</strong> advance in the last decade.</p>
<p>In and of itself it's not really <em>that</em> revolutionary - it's really just a bit of syntax sugar on top of concepts that already existed before (Promises, coroutines, asynchronous IO), but the impact it has is nothing short of staggering. While asynchronous IO was possible before async/await in various ways, it was always difficult and awkward to write such programs. async/await turned that around completely. Suddenly asynchronous IO became trivial to do and this has resulted in <strong>orders of magnitude</strong> performance increases.</p>
<p>About the timeline - although the roots of this idea are much older, the first async/await implementation came in C# in 2012. From this the feature spread rapidly to other languages like Haskell, Python, TypeScript, JavaScript, Rust, Swift and even C++.</p>

CC BY-SA 4.0
2023-09-24T15:12:14.983Z
At least Twisted (Python networking library) had [inlineCallbacks](https://github.com/twisted/twisted/blob/releases/release-8.2.x-3540/twisted/internet/defer.py#L793), an async/await implementation, in 2008. They may have had it even earlier, but I can't track down a precise date.
Corbin
CC BY-SA 4.0
2023-09-28T11:06:33.043Z
The async/await pattern seems to have first appeared in Haskell around 1999 (e.g. [A poor man's concurrency monad](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/poor-mans-concurrency-monad/A369E310ADAE4455020C918FC1D47958)). async/await is a limited form of delimited continuation (like many other 'control-flow pairs', e.g. try/throw, call/early-return, for/yield, etc.); those date back to the 1980s and are commonly used for coroutines (though I'm not sure when the exact pattern of async/await appeared)
Warbo
CC BY-SA 4.0
2023-09-28T11:51:03.020Z
@Warbo I'm... not sure where it fits in the pure theory world. But I also cannot see how one could use, say, try/catch to implement something similar to await/async. I know that there are implementations that (ab)use for/yield, although I think that not every language's for/yield is suited for this purpose either. Anyway they are not as elegant as the dedicated await/async.
Vilx-
CC BY-SA 4.0
2023-09-28T12:20:25.410Z
@Vilx- Sorry, I may have been confusing: "delimited continuations" are a powerful language feature dating back to ~1988; shift/reset is the most common form. If you have shift/reset, you can implement async/await as a library; you can also implement try/catch, for/yield, etc. too. Delimited continuations can be thought of as "resumable exceptions" (related to Algebraic Effects), ["exceptions with state"](https://arxiv.org/pdf/1710.10385.pdf), ["non-linear yield"](http://lambda-the-ultimate.org/node/4349), or ["the mother of all monads"](http://blog.sigfpe.com/2008/12/mother-of-all-monads.html)
Warbo
CC BY-SA 4.0
2023-09-28T12:49:45.290Z
@Warbo - Well, as I said, the base ideas are not new, but it's this particular... manifestation (implementation?) of them that has turned out to be wildly successful.
Vilx-
CC BY-SA 4.0
2023-09-28T15:31:24.340Z
Sure. Whilst delimited continuations have been used for various coroutine patterns since the 80s, I don't know if they were used for the specific pattern we call async/await that long ago (maybe, maybe not).
Warbo
CC BY-SA 4.0
2023-09-28T15:35:32.570Z
Also note that baking these operations into a language with keywords (e.g. `async`/`await` in C#/Python/JS/etc.) was done in the 90s by [the E language](https://en.wikipedia.org/wiki/E_(programming_language)), which called them [`<-`/`when` operators](http://wiki.erights.org/wiki/Walnut/Distributed_Computing#Eventually_Operator) (actually E is also more general, since it allows distributed, parallel programming; if we limit our program to one thread on one machine then <-/when acts just like async/await)
Warbo
CC BY-SA 4.0
2023-09-23T23:52:15.720Z
2023-09-23T23:52:15.720Z
Vilx-
<p>There is a lot going on in cryptography.</p>
<ul>
<li><a href="https://en.wikipedia.org/wiki/Homomorphic_encryption" rel="noreferrer">Homomorphic encryption</a></li>
<li><a href="https://en.wikipedia.org/wiki/Non-interactive_zero-knowledge_proof" rel="noreferrer">Zero-knowledge proofs</a>, snarks and zk-snarks</li>
<li><a href="https://en.wikipedia.org/wiki/Post-quantum_cryptography" rel="noreferrer">Post-quantum cryptography</a></li>
</ul>
<p>This post is community wiki; hopefully others can expand.</p>

CC BY-SA 4.0
2023-09-26T07:10:31.927Z
2023-09-26T07:10:31.927Z
usul
<p>There have been numerous advances in <strong>machine learning</strong> since 2010. Most of the highly impactful advances are not fully theoretically sound, but most of them involve some theoretical backings, to greater and lesser extents.</p>
<ul>
<li>progress in convex and non-convex optimization</li>
<li>game-playing, regret minimization</li>
<li>neural network architectures, evaluation, and training methods</li>
<li>reinforcement learning, recommendation algorithms</li>
</ul>

CC BY-SA 4.0
2023-09-26T07:15:53.753Z
2023-09-26T07:15:53.753Z
usul
<p><a href="https://en.wikipedia.org/wiki/Differential_privacy" rel="noreferrer">Differential privacy</a>, a technique for analyzing data and releasing statistics privately, was in its infancy in 2010 and has since had a lot of development and advances, and adoption by major web browsers for telemetry, the U.S. 2020 Census, and probably numerous other places.</p>

CC BY-SA 4.0
2023-09-26T07:24:26.180Z
2023-09-26T07:24:26.180Z
usul
<p>CRDT (Conflict-free replicated data type), data structure used for decentralized real-time editors, has been formally defined in 2011, according to <a href="https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type" rel="noreferrer">wikipedia</a>. Industry adoption is also mentioned in the same <a href="https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type#Industry_use" rel="noreferrer">wikipedia page</a></p>

CC BY-SA 4.0
2023-09-25T18:07:19.487Z
Yes. Research on the verification of CRDTs and algos based on CRDT is also very active.
Martin Berger
CC BY-SA 4.0
2023-09-25T17:12:51.260Z
2023-09-25T17:12:51.260Z
gexahedron
<p>Since I left school (early 2010s) a couple of recently developed techniques were widely adopted by the industry. For example,</p>
<ul>
<li><a href="https://en.wikipedia.org/wiki/Asymmetric_numeral_systems" rel="noreferrer">Asymmetric  numeral systems</a> for compression (e.g. Ubuntu ships with <code>zstd</code> command line utility which implements ideas from ANS).</li>
<li><a href="https://raft.github.io/" rel="noreferrer">Raft consensus algorithm</a> for consensus in distributed systems, implemented in many widely used systems such as <a href="https://etcd.io/" rel="noreferrer">etcd</a>.</li>
</ul>
<p>are some recent advances in computer science from the last decade that have 1) sound theoretical basis, are 2) implementable, and 3) have achieved some level of adoption in the industry (this last criterion is nice to have but not necessary).</p>
<p>I am interested in other examples that fulfill at least 2 out of the 3 (subjective :-) criteria that I enumerated. (For example, a new technique that has both (1) and (2) but has not yet been adopted is something I'd like to know about.)</p>

CC BY-SA 4.0
2023-09-23T13:02:57.880Z
Bounded model checking, using SAT/SMT-solvers in model checking. Example: https://github.com/diffblue/cbmc
Martin Berger
CC BY-SA 4.0
2023-09-23T13:05:04.313Z
Linear / affine types (Rust)
Martin Berger
CC BY-SA 4.0
2023-09-23T13:07:23.227Z
Fuzzing, too many reference to mention, see e.g. https://cacm.acm.org/magazines/2020/2/242350-fuzzing/abstract
Martin Berger
CC BY-SA 4.0
2023-09-23T13:10:23.203Z
Effect systems / types, e.g. in Ocaml v 5.0 https://v2.ocaml.org/manual/effects.html or https://www.eff-lang.org/
Martin Berger
CC BY-SA 4.0
2023-09-23T13:13:41.280Z
Hardware acceleration for guaranteed (spatial) memory safety, e.g. CHERI https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-951.pdf
Martin Berger
CC BY-SA 4.0
2023-09-23T15:27:44.527Z
Various forms of gradual typing, to enable static and dynamic types to work together. Most prominent example: TypeScript.
Martin Berger
CC BY-SA 4.0
2023-09-25T09:29:24.003Z
@MartinBerger Bounded Model Checking has been around since the late 1990's, hasn't it?
Jan Johannsen
CC BY-SA 4.0
2023-09-25T09:33:56.903Z
@JanJohannsen Yes, model checking is much older. *Bounded* model checking was introduced in the paper *"Symbolic Model Checking without BDDs"* (1999) by Biere et al, but I think SAT/SMT solvers only really became fast enough to be used in large-scale verification in the last decade or so.
Martin Berger
CC BY-SA 4.0
2023-09-25T09:54:41.407Z
@MartinBerger Yes, I was thinking of that paper. AFAIR the solver zchaff released in 2002 was already suitable to be used for that purpose.
Jan Johannsen
CC BY-SA 4.0
2023-09-25T10:00:49.940Z
@JanJohannsen Thanks for reminding me.
Martin Berger
CC BY-SA 4.0
2023-09-25T16:20:13.340Z
I feel one idea in Raft is often overlooked: the fact that it was explicitly designed to be *understandable* and *teachable*. We are used to have algorithms designed to be *correct* and to be optimized for certain kinds of performance metrics (throughput, latency, memory usage, power consumption), to be resistant to certain kinds of attacks, etc. But simplicity, teachability, and understandability are usually not explicit design goals. I am not aware whether this is a *new* contribution by Raft, but it is an important one. How many algorithm papers contain a user study?
Jörg W Mittag
CC BY-SA 4.0
2023-09-25T23:59:14.630Z
One could include things like Secure Computation (both MPC and FHE) and Zero Knowledge proofs from cryptography as well.
Mark Schultz-Wu
CC BY-SA 4.0
2023-09-26T07:19:09.743Z
"have achieved some level of adoption in the industry (this last criterion is nice to have but not necessary)." -- Without this criterion, you are just asking for a list of all 'implementable' papers in theoretical CS since 2010, which seems a bit broad even to me.
usul
<ds.algorithms><soft-question><ds.data-structures><se.software-engineering>
Recent advances in computer science since 2010?
user12344567
# Recent advances in computer science since 2010?

(Asked by: username_0 on 2023-09-23)

Since I left school (early 2010s) a couple of recently developed techniques were widely adopted by the industry. For example,

* [Asymmetric numeral systems](https://en.wikipedia.org/wiki/Asymmetric_numeral_systems) for compression (e.g. Ubuntu ships with `zstd` command line utility which implements ideas from ANS).
* [Raft consensus algorithm](https://raft.github.io/) for consensus in distributed systems, implemented in many widely used systems such as [etcd](https://etcd.io/).

are some recent advances in computer science from the last decade that have 1) sound theoretical basis, are 2) implementable, and 3) have achieved some level of adoption in the industry (this last criterion is nice to have but not necessary).

I am interested in other examples that fulfill at least 2 out of the 3 (subjective :-) criteria that I enumerated. (For example, a new technique that has both (1) and (2) but has not yet been adopted is something I'd like to know about.)

**Tags:** ds.algorithms, soft-question, ds.data-structures, se.software-engineering
> **Comments:**
> **username_1**: Bounded model checking, using SAT/SMT-solvers in model checking. Example: https://github.com/diffblue/cbmc  
> **username_1**: Linear / affine types (Rust)  
> **username_1**: Fuzzing, too many reference to mention, see e.g. https://cacm.acm.org/magazines/2020/2/242350-fuzzing/abstract  
> **username_1**: Effect systems / types, e.g. in Ocaml v 5.0 https://v2.ocaml.org/manual/effects.html or https://www.eff-lang.org/  
> **username_1**: Hardware acceleration for guaranteed (spatial) memory safety, e.g. CHERI https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-951.pdf  
> **username_1**: Various forms of gradual typing, to enable static and dynamic types to work together. Most prominent example: TypeScript.  
> **username_2**: @MartinBerger Bounded Model Checking has been around since the late 1990's, hasn't it?  
> **username_1**: @JanJohannsen Yes, model checking is much older. *Bounded* model checking was introduced in the paper *"Symbolic Model Checking without BDDs"* (1999) by Biere et al, but I think SAT/SMT solvers only really became fast enough to be used in large-scale verification in the last decade or so.  
> **username_2**: @MartinBerger Yes, I was thinking of that paper. AFAIR the solver zchaff released in 2002 was already suitable to be used for that purpose.  
> **username_1**: @JanJohannsen Thanks for reminding me.  
> **username_3**: I feel one idea in Raft is often overlooked: the fact that it was explicitly designed to be *understandable* and *teachable*. We are used to have algorithms designed to be *correct* and to be optimized for certain kinds of performance metrics (throughput, latency, memory usage, power consumption), to be resistant to certain kinds of attacks, etc. But simplicity, teachability, and understandability are usually not explicit design goals. I am not aware whether this is a *new* contribution by Raft, but it is an important one. How many algorithm papers contain a user study?  
> **username_4**: One could include things like Secure Computation (both MPC and FHE) and Zero Knowledge proofs from cryptography as well.  
> **username_5**: "have achieved some level of adoption in the industry (this last criterion is nice to have but not necessary)." -- Without this criterion, you are just asking for a list of all 'implementable' papers in theoretical CS since 2010, which seems a bit broad even to me.  

---

## 10 answers

### Answer by username_1 on 2023-09-23. Score: 35

**Deriving fast JIT compilers from interpreters.** It has long been known, that, in principle, compilers can be derived
from interpreters in a mechanical way. This is a special case of
partial evaluation, sometimes called *Futamura projection* [1]. The
textbook [2] explains the state-of-the-art at the end of the 1990s.
The core problem is that it has been difficult to get compilers derived
by partial evaluation to match the performance of handwritten
compilers (*"O, Partial Evaluator, Where Art Thou?"* L. Augustsson, 2010).
In a parallel development, (tracing) JIT compilers emerged, their
convoluted development might have started with [3]. The core problem
with (tracing) JIT compilers is that they are complex, and
expensive to develop.

Over the last few years, the situation changed.

* Meta-tracing was developed [4]
  which turns an annotated interpreter into a tracing JIT compiler. This is the
  basis of PyPy [5] which is widely used [9].
* In a parallel development, Oracle's new approach to Java compilation, Graal/Truffle
  [6, 7, 8], is based on partial evaluation, and indeed uses Futamura
  projections to convert an interpreter into a compiler (Graal is a
  conventional JIT and Truffle does the Futamura projection). It has
  been claimed that this is the first time that partial evaluation
  Futamura projection has led to a performant compiler.

There is clearly some family resemblance between meta-tracing and partial evaluation, but the exact relationship, the shared abstraction, is not fully understood.

---

[1] Y. Futamura, *Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler.*

[2] J. Jones, C. K. Gormand, P. Sestoft, *Partial Evaluation and Automatic Program Generation.*

[3] J. G. Mitchell, *The design and construction of flexible and efficient interactive programming systems.*

[4] C. F. Bolz, A. Cuni, M. Fijalkowski, A. Rigo, *Tracing the Meta-Level: PyPy's Tracing JIT Compiler.*

[5] <https://www.pypy.org/>

[6] T. Würthinger, C. Wimmer, C. Humer, A. Wöß, L. Stadler, C. Seaton, G. Duboscq, D. Simon, M. Grimmer, *Practical partial evaluation for high-performance dynamic language runtimes.* <https://chrisseaton.com/truffleruby/pldi17-truffle/pldi17-truffle.pdf>

[7] <https://github.com/oracle/graal/tree/master>

[8] <https://github.com/oracle/graal/tree/master/truffle>

[9] <https://news.ycombinator.com/item?id=36940871>

> **Comments:**
> **username_6**: The first usable version of PyPy was released in 2007; paper [4] (link [here](https://dl.acm.org/doi/10.1145/1565824.1565827)) was published in 2009. For clarity, it would be better to talk about RPython, the toolkit which builds PyPy; this toolkit was isolated in the early 2010s and is now available as a standalone package for non-PyPy usage.  
> **username_7**: I recomend this book https://www.itu.dk/people/sestoft/pebook/  

---

### Answer by username_1 on 2023-09-23. Score: 20

**Low precision floating point data types.** Historically, most programming used the IEEE 754 Standard for
Floating-Point Arithmetic. Simplifying a great deal, IEEE 754 floats (64 bits version) give you

* Lot of precision (53 bits mantissa).
* Small exponent: 11 bits.

Historically, this was a good choice for many applications at the time. But it turns out that this was not good for deep learning. Simplifying a great deal:

* Needs lots of memory for each floating point number.
* Small exponent is problematic, because during training we often
  encounter extremely large or extremely small values.
* High precision leads to overfitting, since high precision is a form
  of model capacity Having low precision arithmetic can be seen as a
  form of regularisation.
* Maybe most important is the hardware perspecive:

  + Multiplication of exponents uses $O(n)$
    transistors in the size of the exponent (multiplication of exponents is done by adding),
  + Multiplication of mantissa uses $O(n^2)$
    transistors in the size of the mantissa.

By using less precision (mantissa) but bigger exponents we need
fewer transistors per (floating point) arithmetic unit in processors,
so we can pack more arithmetic units into each processor, which
increases FP performance. This lead to experimentation and Google's first TPU uses
the `bfloat16` floating-point format

* Sign bit: 1 bit
* Exponent width: 8 bits
* Mantissa: 7 bits
* Different handling of underflows, overflows, and NaNs.

This lead to a flurry of activity, and modern CPUs and GPUs all
provide for such low precision floating point numbers.

Given the preponderance of arithmetic units for low precision floating point arithmetic in modern processors, an interesting question is: how efficiently to bootstrap
high-precision floating point operations from low precision floats?

(Note: I'm not sure about the history of low precision floats, that's why I'm not adding references. Feel free to edit.)

> **Comments:**
> **username_8**: I don't see how that's a CS advance. For as long as FP have existed you could have made them with larger exponents and smaller mantissas.  
> **username_1**: @toasted_flakes You can simulate the new short floats, but that would be *much less* efficient than having them as hardware primitives, presumably orders of magnitude less (just think about memory usage of your scheme, or transistors that are needed for IEEE 754 float multiplication vis-a-vis bfloat16). So I don't think you can simulate using comparable memory and transistor budget. Also, we have empirical evidence about the effect of different float formats on deep learning. None of this existed until recently.  
> **username_9**: @toasted_flakes: I agree, it's not a new advance in computer **science**, it's just a case of different engineering tradeoffs for the same basic format becoming useful (and commercially relevant) for a new problem domain.  The "science" part of this is the observation that deep-learning still works fine with few mantissa bits, enabling us to make that different engineering choice for an already-known approach to representing real numbers with fixed bit width.  
> **username_9**: @toasted_flakes: A *new* approach to representing real numbers is the Posit, which avoids spending coding space on NaNs and Inf, and has gradual *overflow* for more dynamic range in limited bits, vs. IEEE FP having gradual underflow (subnormals) but hard overflow to +Inf.  https://spectrum.ieee.org/floating-point-numbers-posits-processor / https://www.johndcook.com/blog/2018/04/11/anatomy-of-a-posit-number/   Posit support is even more limited in hardware that bfloat or IEEE FP16, but apparently Posit FPUs aren't too expensive to build.  

---

### Answer by username_1 on 2023-09-23. Score: 20

**Liquid types.** Introduced in [1], and refined in multiple follow-up papers. Liquid types can be seen as a form of dependent types that break with
traditional type theory which is keen to
have 'nice' typing rules that can be seen logical rules (this is the Curry-Howard
perspective). Instead, liquid types are developed with a view towards maximising automation: all constraints during type-inference are simply
handed to an SMT-solver, and automatically solved.

Liquid types are now used in industry for processor specification and
verification through the Sail language [2], which is widely used, most prominently, for specifying the RISC-V instruction
set architecture [3]. There are concerted efforts at augmenting
general purpose languages with liquid types, in particular

* Haskell [4]
* Rust [5]

and probably more that I am not aware of.

(I used to be sceptical of using types much stronger than Damas-Hindley-Milner style *Let-Polymorphism* in general-purpose programming languages due to the loss of convenient type inference. Liquid types changed my mind.)

---

1. P. M. Rondon, M. Kawaguchi, R. Jhala, *Liquid Types.* [https://goto.ucsd.edu/~rjhala/papers/liquid\_types.html](https://goto.ucsd.edu/%7Erjhala/papers/liquid_types.html)
2. A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray,
   M. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur,
   I. Stark, N. Krishnaswami, P. Sewell, *ISA Semantics for ARMv8-A,
   RISC-V, and CHERI-MIPS.* <https://github.com/rems-project/sail>
3. <https://github.com/riscv/sail-riscv>
4. <https://ucsd-progsys.github.io/liquidhaskell/>
5. N. Lehmann, A. Geller, N. Vazou, R. Jhala, Flux: *Liquid Types for Rust.* <https://github.com/flux-rs/flux>

> **Comments:**
> **username_10**: Do you know if/how this relates to [F*](https://fstar-lang.org/)? F* is all about dependent types and using an SMT solver, but I have no idea if that's the same or different approach.  
> **username_1**: @cubuspl42 Not in detail. Both F* liquid types are based on refinement types, but F*'s are more powerful, in that F* does *not* only support type-based reasoning about programs, unlike liquid types.  

---

### Answer by username_11 on 2023-09-24. Score: 16

**Newer data structures**. The mighty Bloom filter, which has been around since 1970, provides a way to store an approximation of a set of $n$ elements with false positive rate $\varepsilon$ using approximately $1.44 n \log\_2 \varepsilon$ bits. In 2014 the cuckoo filter, based on cuckoo hashing, provided an alternative using approximately $1.08 n \log\_2 \varepsilon + 3n$ bits while supporting deletions, while the 2019 [XOR filter](https://stackoverflow.com/questions/67527507/what-is-an-xor-filter) supports the set in $1.23 n \log\_2 \varepsilon$ bits. While a full analysis of cuckoo filters is still open as of 2023, the theoretical basis for XOR filters is decently well understood and the connection to hypergraph peeling and orientability led to further improvements (most famously the Ribbon filter, which has been used at scale at Meta).

In 2017 the zip tree was invented, providing a way to build a randomized balanced binary search tree using $O(\log \log n)$ random bits per element. The height of zip trees slightly exceeds that of treaps, but in 2023 the zip-zip tree was introduced, which matches the theoretical guarantees of treaps using only $O(\log \log n)$ bits of randomness per element. To the best of my knowledge this data structure isn’t used in practice, but it’s definitely worth a look.

Just missing your cutoff, in 2009 the SA-IS algorithm for building suffix arrays was introduced. It runs in time $O(n)$ and is quite fast in practice. One of the most widely used suffix array construction algorithm libraries (LibDivSufSort) is based on the techniques developed in this algorithm.

> **Comments:**
> **username_12**: [Hollow heaps](https://arxiv.org/abs/1510.06535) (2015) are another example of a direct improvement over an existing data structure.  
> **username_11**: I’ve heard of hollow heaps but wasn’t aware that they were an improvement over other data structures. Can you elaborate? (I teach a course on “advanced” data structures and am always looking to modernize the syllabus!)  
> **username_12**: Hollow heaps provide the same asymptotics as Fibonacci heaps, but improve the constant factors, which afaik are so high for the latter that it is never used in practice.  

---

### Answer by username_1 on 2023-09-23. Score: 15

**Translation validation of compilers.**
In compilation, especially optimising compilation, correctness is a big issue for obvious reasons.
Ideally, we'd like the whole compiler being proven correct once and for all, but this is beyond the state-of-the-art in 2023 for
industrial strength compilers like LLVM and GCC (still there is progress, see CompCert [1]
CakeML [2]).

However, we should not let the perfect be the enemy of the good: enter *translation validation* [3]. The idea is simple:
instead of giving a **single** proof that the compiler is correct for **all** input programs $P$, we prove, for an individual program $P$ that the translation of
$P$ is correct. This is much less demanding. Note that proving that the compiler correctly translates a given program $P$, does *not* imply that it
also translates other programs correctly! That may sound really weak, but, empirically, translation validation is useful [4, 5, 6]:

* Translation validation (at least of individual optimisation passes) can be automated with SMT solvers like Z3, even for complex LLVM optimisation passes.
* Doing translation validation for a modest size number of programs finds huge number of bugs in complex LLVM optimisation passes automatically

This raises more questions: for example, is the translation validator itself correct? See [7] for recent progress in this direction.

---

[1] X. Leroy, *Formal verification of a realistic compiler.* <https://xavierleroy.org/publi/compcert-CACM.pdf>

[2] <https://cakeml.org/>

[3] A. Pnueli, M. Siegel, E. Singerman, *Translation Validation.*

[4] N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr, *Provably Correct Peephole Optimizations with Alive.*

[5] N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, J. Regehr, *Alive2: Bounded Translation Validation for LLVM.*

[6] <https://github.com/AliveToolkit/alive2>

[7] J. Lee, C.-K. Hur, N. P. Lopes, *AliveInLean: A Verified LLVM Peephole Optimization Verifier.*


---

### Answer by username_13 on 2023-09-23. Score: 15

### async/await pattern

I'm not really sure how well this fits the criteria (especially the "since 2010" part is kinda fuzzy here), but I myself consider this to be the most significant **practical** advance in the last decade.

In and of itself it's not really *that* revolutionary - it's really just a bit of syntax sugar on top of concepts that already existed before (Promises, coroutines, asynchronous IO), but the impact it has is nothing short of staggering. While asynchronous IO was possible before async/await in various ways, it was always difficult and awkward to write such programs. async/await turned that around completely. Suddenly asynchronous IO became trivial to do and this has resulted in **orders of magnitude** performance increases.

About the timeline - although the roots of this idea are much older, the first async/await implementation came in C# in 2012. From this the feature spread rapidly to other languages like Haskell, Python, TypeScript, JavaScript, Rust, Swift and even C++.

> **Comments:**
> **username_6**: At least Twisted (Python networking library) had [inlineCallbacks](https://github.com/twisted/twisted/blob/releases/release-8.2.x-3540/twisted/internet/defer.py#L793), an async/await implementation, in 2008. They may have had it even earlier, but I can't track down a precise date.  
> **username_14**: The async/await pattern seems to have first appeared in Haskell around 1999 (e.g. [A poor man's concurrency monad](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/poor-mans-concurrency-monad/A369E310ADAE4455020C918FC1D47958)). async/await is a limited form of delimited continuation (like many other 'control-flow pairs', e.g. try/throw, call/early-return, for/yield, etc.); those date back to the 1980s and are commonly used for coroutines (though I'm not sure when the exact pattern of async/await appeared)  
> **username_13**: @Warbo I'm... not sure where it fits in the pure theory world. But I also cannot see how one could use, say, try/catch to implement something similar to await/async. I know that there are implementations that (ab)use for/yield, although I think that not every language's for/yield is suited for this purpose either. Anyway they are not as elegant as the dedicated await/async.  
> **username_14**: @Vilx- Sorry, I may have been confusing: "delimited continuations" are a powerful language feature dating back to ~1988; shift/reset is the most common form. If you have shift/reset, you can implement async/await as a library; you can also implement try/catch, for/yield, etc. too. Delimited continuations can be thought of as "resumable exceptions" (related to Algebraic Effects), ["exceptions with state"](https://arxiv.org/pdf/1710.10385.pdf), ["non-linear yield"](http://lambda-the-ultimate.org/node/4349), or ["the mother of all monads"](http://blog.sigfpe.com/2008/12/mother-of-all-monads.html)  
> **username_13**: @Warbo - Well, as I said, the base ideas are not new, but it's this particular... manifestation (implementation?) of them that has turned out to be wildly successful.  
> **username_14**: Sure. Whilst delimited continuations have been used for various coroutine patterns since the 80s, I don't know if they were used for the specific pattern we call async/await that long ago (maybe, maybe not).  
> **username_14**: Also note that baking these operations into a language with keywords (e.g. `async`/`await` in C#/Python/JS/etc.) was done in the 90s by [the E language](https://en.wikipedia.org/wiki/E_(programming_language)), which called them [`<-`/`when` operators](http://wiki.erights.org/wiki/Walnut/Distributed_Computing#Eventually_Operator) (actually E is also more general, since it allows distributed, parallel programming; if we limit our program to one thread on one machine then <-/when acts just like async/await)  

---

### Answer by username_5 on 2023-09-26. Score: 7

There is a lot going on in cryptography.

* [Homomorphic encryption](https://en.wikipedia.org/wiki/Homomorphic_encryption)
* [Zero-knowledge proofs](https://en.wikipedia.org/wiki/Non-interactive_zero-knowledge_proof), snarks and zk-snarks
* [Post-quantum cryptography](https://en.wikipedia.org/wiki/Post-quantum_cryptography)

This post is community wiki; hopefully others can expand.


---

### Answer by username_5 on 2023-09-26. Score: 5

[Differential privacy](https://en.wikipedia.org/wiki/Differential_privacy), a technique for analyzing data and releasing statistics privately, was in its infancy in 2010 and has since had a lot of development and advances, and adoption by major web browsers for telemetry, the U.S. 2020 Census, and probably numerous other places.


---

### Answer by username_15 on 2023-09-25. Score: 5

CRDT (Conflict-free replicated data type), data structure used for decentralized real-time editors, has been formally defined in 2011, according to [wikipedia](https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type). Industry adoption is also mentioned in the same [wikipedia page](https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type#Industry_use)

> **Comments:**
> **username_1**: Yes. Research on the verification of CRDTs and algos based on CRDT is also very active.  

---

### Answer by username_5 on 2023-09-26. Score: 4

There have been numerous advances in **machine learning** since 2010. Most of the highly impactful advances are not fully theoretically sound, but most of them involve some theoretical backings, to greater and lesser extents.

* progress in convex and non-convex optimization
* game-playing, regret minimization
* neural network architectures, evaluation, and training methods
* reinforcement learning, recommendation algorithms


---

