<p>Taking a liberal view of TCS, I can think of the following, all of which have profound influence on theoretical and practical computing.</p>
<ul>
<li>The Spectre vulnerability (which undermines speculation, a (the) core principle behind the performance of all modern CPUs).</li>
<li>Strassen's fast matrix multiplication algorithm.</li>
<li>Scott's model of the untyped <span class="math-container">$\lambda$</span>-calculus.</li>
<li>Gödel's incompleteness theorems.</li>
</ul>
<p>An additional surprise, but not a single result, is the usefulness of SAT/SMT solvers in practice, which has lead to the the surprising realisation that SAT is the paradigm case of a feasible complexity class. TCS has not yet caught up with this.</p>

CC BY-SA 4.0
2024-01-28T10:04:24.550Z
For Dana Scott, he told me he was developing  semantics of *typed* languages to show people how and why types were advantageous – but his setup also turned out to give semantics to the untyped ones. So, that's definitely a surprise, but he wasn't "trying to prove the opposite" (which would be "the untyped λ-calculus does not have a semantics").
Andrej Bauer
CC BY-SA 4.0
2024-01-28T10:11:53.257Z
@AndrejBauer That's interesting. 
I seem to recall having read somewhere 
that Scott tried to prove that the impossibility of such a model from the
set-theoretic fact that no interesting set $D$ and be isomorphic to its own function space (set theoretically).
You have a much better connection to Dana Scott than me, so I've removed the remark about trying to prove  the opposite.
Martin Berger
CC BY-SA 4.0
2024-01-28T10:15:36.473Z
Well, he never told me that he *didn't* try to prove non-existence of the model, but I would be surprised. Since it had been known from Church-Rosser that the $\lambda$-calclus is consistent, it would have a model on general grounds (the Lindenbaum-Tarski algebra, more or less). I asked Dana something along the lines of "but Church-Rosses tells us $\lambda$-calculus is consistent", to which his response was "but what does it *mean*?" So I think it's more about findin *the right kind* of model than just any model.
Andrej Bauer
CC BY-SA 4.0
2024-01-28T10:20:33.093Z
@AndrejBauer Maybe you can ask him?
Martin Berger
CC BY-SA 4.0
2024-01-28T10:50:20.917Z
Sure, I can do it.
Andrej Bauer
CC BY-SA 4.0
2024-01-28T09:23:38.137Z
2024-01-28T10:11:38.233Z
2024-01-28T10:11:38.233Z
Martin Berger
<p>Robin Milner's <span class="math-container">$\nu$</span> operation, which abstracts and axiomatises the ability to generate    fresh names at will in a (quasi-)compositional way.</p>
<p>Naming is a long-standing problem in computer science. Most
programming languages can define naming constructs, which, when
called, yield a fresh name.  This seemed like a completely marginal
issue, and was given little attention. After all, you could implement
it as a global variables. But only with Milner's axiomatisation, and
use in <span class="math-container">$\pi$</span>-calculus, were the profound structural implications of
free name generations discovered, including how we approach the mechanised foundations of mathematics (e.g. nominal logic).</p>

CC BY-SA 4.0
2024-01-28T09:37:02.653Z
2024-01-28T09:37:02.653Z
Martin Berger
<p>I was recently listening to Sean Carroll's <a href="https://www.youtube.com/watch?v=qD4XkFndaFk&amp;t=6080s" rel="nofollow noreferrer">interview</a> with Scott Aaronson, and the two of them briefly talked about surprises in their respective fields (theoretical and particle physics, and theoretical computer science).  They both agreed that some surprises would be so abnormal that they would be immediately suspicious, while other, less earth-shattering surprises have indeed happened in both of their fields.</p>
<p>I guess superluminal neutrinos, respectively the collapse of the polynomial hierarchy, would be in the first category, while Madame Wu's <a href="https://en.wikipedia.org/wiki/Wu_experiment" rel="nofollow noreferrer">experiment</a> showing violation of P-symmetry, respectively the proof of IP=PSPACE, have a similar feel as representatives of the second category.  I was thinking that theoretical physicists coyly ask &quot;<a href="https://pubs.aip.org/physicstoday/article/54/1/68/411575/Theory-Phenomenology-and-Who-Ordered-That" rel="nofollow noreferrer">who ordered that</a>&quot; when they have evidence that requires a significant update in their priors.</p>
<p>I think perhaps Impagliazzo and Wigderson's results on P and BPP (and, analogously, NP and AM) have a similar vibe and gave many theoretical computer scientists pause.  What other theoretical computer science results have that same feel?</p>

CC BY-SA 4.0
2024-01-26T20:34:00.593Z
Candidates: PRIMES in P, PCP theorem, Ramanujan expanders, Unique Games.
usul
CC BY-SA 4.0
2024-05-13T02:11:46.920Z
Thanks! Was the derandomization of PRIMES *surprising?* (AKS is brilliant and rightfully deserves all the praise of course… with some analogy to LIGO’s discovery…)
Mark S
<soft-question><big-picture><ho.history-overview>
What are some "who ordered that?" moments in theoretical computer science?
Mark S
# What are some "who ordered that?" moments in theoretical computer science?

(Asked by: username_0 on 2024-01-26)

I was recently listening to Sean Carroll's [interview](https://www.youtube.com/watch?v=qD4XkFndaFk&t=6080s) with Scott Aaronson, and the two of them briefly talked about surprises in their respective fields (theoretical and particle physics, and theoretical computer science). They both agreed that some surprises would be so abnormal that they would be immediately suspicious, while other, less earth-shattering surprises have indeed happened in both of their fields.

I guess superluminal neutrinos, respectively the collapse of the polynomial hierarchy, would be in the first category, while Madame Wu's [experiment](https://en.wikipedia.org/wiki/Wu_experiment) showing violation of P-symmetry, respectively the proof of IP=PSPACE, have a similar feel as representatives of the second category. I was thinking that theoretical physicists coyly ask "[who ordered that](https://pubs.aip.org/physicstoday/article/54/1/68/411575/Theory-Phenomenology-and-Who-Ordered-That)" when they have evidence that requires a significant update in their priors.

I think perhaps Impagliazzo and Wigderson's results on P and BPP (and, analogously, NP and AM) have a similar vibe and gave many theoretical computer scientists pause. What other theoretical computer science results have that same feel?

**Tags:** soft-question, big-picture, ho.history-overview
> **Comments:**
> **username_1**: Candidates: PRIMES in P, PCP theorem, Ramanujan expanders, Unique Games.  
> **username_0**: Thanks! Was the derandomization of PRIMES *surprising?* (AKS is brilliant and rightfully deserves all the praise of course… with some analogy to LIGO’s discovery…)  

---

## 2 answers

### Answer by username_2 on 2024-01-28. Score: 3

Taking a liberal view of TCS, I can think of the following, all of which have profound influence on theoretical and practical computing.

* The Spectre vulnerability (which undermines speculation, a (the) core principle behind the performance of all modern CPUs).
* Strassen's fast matrix multiplication algorithm.
* Scott's model of the untyped $\lambda$-calculus.
* Gödel's incompleteness theorems.

An additional surprise, but not a single result, is the usefulness of SAT/SMT solvers in practice, which has lead to the the surprising realisation that SAT is the paradigm case of a feasible complexity class. TCS has not yet caught up with this.

> **Comments:**
> **username_3**: For Dana Scott, he told me he was developing  semantics of *typed* languages to show people how and why types were advantageous – but his setup also turned out to give semantics to the untyped ones. So, that's definitely a surprise, but he wasn't "trying to prove the opposite" (which would be "the untyped λ-calculus does not have a semantics").  
> **username_2**: @AndrejBauer That's interesting.  I seem to recall having read somewhere  that Scott tried to prove that the impossibility of such a model from the set-theoretic fact that no interesting set $D$ and be isomorphic to its own function space (set theoretically). You have a much better connection to Dana Scott than me, so I've removed the remark about trying to prove  the opposite.  
> **username_3**: Well, he never told me that he *didn't* try to prove non-existence of the model, but I would be surprised. Since it had been known from Church-Rosser that the $\lambda$-calclus is consistent, it would have a model on general grounds (the Lindenbaum-Tarski algebra, more or less). I asked Dana something along the lines of "but Church-Rosses tells us $\lambda$-calculus is consistent", to which his response was "but what does it *mean*?" So I think it's more about findin *the right kind* of model than just any model.  
> **username_2**: @AndrejBauer Maybe you can ask him?  
> **username_3**: Sure, I can do it.  

---

### Answer by username_2 on 2024-01-28. Score: 2

Robin Milner's $\nu$ operation, which abstracts and axiomatises the ability to generate fresh names at will in a (quasi-)compositional way.

Naming is a long-standing problem in computer science. Most
programming languages can define naming constructs, which, when
called, yield a fresh name. This seemed like a completely marginal
issue, and was given little attention. After all, you could implement
it as a global variables. But only with Milner's axiomatisation, and
use in $\pi$-calculus, were the profound structural implications of
free name generations discovered, including how we approach the mechanised foundations of mathematics (e.g. nominal logic).


---

