> slow-ban

I, too, can't post as many messages as I'd like. Not sure why, or how
to change it, or how even to see if there's some limit imposed on
me. Maybe < 1000 rep users are throttled?

> Maybe they're not ready for a compilers course then?

We've been teaching compilers to 2nd years ever since the department
was founded as far as I'm aware. The 2nd year is the right time to see how the
programmer's most important tool works.

> you don't have to roll out your own.

I want students to write their own lexer and parser, and familiarise
themselves with lexer/parser generators. This is an important part of
a programmer's education. First, it let's them see the purpose of all
that formal language theory they had to do in the first year. Second,
and more important, working programmers have to design languages and
write lexers/parsers all the time. A lot of commercial programming is
about transforming data from one representation to another. In
contrast, few programmers will ever write a real code generator.

> you're teaching in a lunatics asylum

I teach at a large, well-known and decidedly mediocre university. The
kind of place that most working programmers graduate from. Needless to
say that this is perfectly compatible with being a lunatics asylum.

> truly efficient concurrent language is always very much
> platform-specific

Sure, but so what? That's like saying for truly efficient concurrent
programming you need to program in assembly, because that's the only
way to exploit all platform specific trickery.

The purpose of high-level languages is to abstract away from the
target platform. The additional goal of languages like C is to
abstract as little as possible, so as to be platform independent while
still allowing fast executables.

In practise compilers for high-performance languages like C/C++ and
Rust need to balance 3 contradictory goals.

- Platform independence.
- Fast executables.
- Low cost of compiler development and evolution.

Note that optimisations are by far the most expensive part of a
compiler. Memory models are used in this balance: you want MMs that
are platform agnostic, while still enabling powerful
compiler optimisations. The CPU vendor has two more objectives (which
is closely related to platform agnosticism):

- Not giving away too many CPU internals.
- Allowing CPU evolution.

> Coq/HOL/ACL2 precise memory models

Are they low-level models of CPUs that can also be used to reason
about read/write reordering? Or are they genuine memory models,
coming from the CPU manufacturers?

As far as I'm aware, the construction of memory models these days is
an empirical science like zoology, where people run experiments to
confirm hypotheses about CPU behaviour. See eg. [1]

> A very practical compiler can also be built as a beautiful and simple pipeline.

Yes, and GHC is probably an example of this. But GHC is not simple by any stretch of the imagination.

M Odersky once gave a talk (sorry, no reference handy) where he said
that scalac, the Scala compiler, is no longer a pipeline, but has
a database structure. That's because scalac's many stages cannot just live on
the data feed by the immediate preceeding stage, and need to go back serveral stages sometime. Interesting.

> you do not need a Turing-complete language to write a compiler.

Type checking / inference in Haskell, Scala and C++ (among others) is
Turing complete. Haskell's compile-time meta-programming extension
Template Haskell, or scala.meta allow you to perform arbitrary
computations as part of the code generation process, and do so by
recursively invoking itself.

On top of this, the control of a Turing machine is a finite state
automata. So it's very simple too.

Finally, I don't see the significance of Turing completeness here.
You can write highly complicated programs in small fragments of Turing
complete languages (e.g. Calculus of Constructions). This is the point
of "Total Functional Programming" [2]. Indeed almost everything the
typical working programmer writes is primitive recursive. Why do we
have Turing complete programming languages? Because using just
primitive recursion is really inconvenient. Try writing a trivial
4-line program like the ancient algorithm computing the greatest
common denominator using just primitive recursion [3]. It's already
annoying. So unrestricted recursion is a convenience, making programs
more readable and shorter. Imagine you had to write type inferencers,
graph-colouring based register allocators or program analyses based on
fix-point iteration using just primitive recursion. Ugh!

> some primitive form of term rewriting of a single input tree into a single output tree.

Term rewriting is Turing complete. So yes, you can transform any
compiler into a term rewriting system. So what? If you transform a
sophisticated, industrial-strength compiler like GHC or scalac into a
TRS, you end up with a very complex TRS that is difficult to
understand. You cannot hide intrinsic complexity. You can kick the can
down the road, and change the form in which the complexity manifests
itself.

> Such a chain is as simple as its most complex building block.

Consider the Turing complete language {S, K} of combinators. By your
reasoning any program written as SK combinators should be simple,
because the building block are trivial.

> JIT is a totally different beast

Not really. In a way, JITs are simpler than AOTs in that the optimisations they
run are simpler (eg register alloc by linear scan rather than graph
colouring), and tracing JIT optimisations are simpler still since they
traces they work on have linear control flow, which drastically
simplifies the optimisation. Indeed that's the point of traces. The
main complication of JITs is the seamless switching between
interpretation and execution of compiled fragments.

> existing JITs are idiotically, needlessly overcomplicated.

Extraordinary claims require extraordinary evidence.

The JIT teams at Oracle, Google, or Microsoft would like to hear from
you if you can lower the cost of JIT compiler construction.

> nanopass compilers are ...

I have nothing against nano-pass compilers, and using a lot of
immutable datastructures is fine. IIRC ocamlopt is heavily based on
immutability, and it's one of the fastest compilers around. Whether
nanopass is better for formal reasoning about compiler correctness
remains to be seen. In formal reasoning it doesn't actually matter
that much if information is passed explicitly by argument, or is
global state, since either way, your logic has to keep track of it.

But whether nano- or otherwise, the complexity is intrinsic in the
problem of compilation, which is about bridging the semantic gap
between two languages. And the bigger the semantic gap, the more
complicated the task.

[1] J. Alglave et al., Herding cats: Modelling, Simulation, Testing, and Data-mining for Weak Memory. http://www0.cs.ucl.ac.uk/staff/J.Alglave/papers/toplas14.pdf

[2] D. A. Turner, Total Functional Programming. http://sblp2004.ic.uff.br/papers/turner.pdf

[3] R. Harper, Old neglected theorems are still theorems. https://existentialtype.wordpress.com/2014/03/20/old-neglect...