3 ms·

A counter example for this would be Haskell. Before Haskell most of the researchers in functional languages started by defining CPU instruction set, then added

A counter example for this would be Haskell. Before Haskell most of the researchers in functional languages started by defining CPU instruction set, then added their programming language, defined how backend of the compilation works and only after that they presented their point. This is sort of situation we see here. Then Haskell came. They presented a nice language based on something others were familiar with (lambda calculus). Since then, two interesting things happened as I understand it. Poeple started adding more nuanced optimization to lambda claculus based backend. This is similar to what LLVM does. Second thing is that instead of comming up with their own languages, most adopted Haskell-style syntax. Just look at modern of functional languages. The mostly look like Haskell (well, ML).

cormacrelf 3y ago
You seem to be implying these researchers are reinventing the wheel by making a syntax that isn't based on anything that's already implemented (like Haskell). That couldn't be further from it. The syntax is absolutely unimportant to a paper like this. Choosing to use curly braces is their version of naming a variable "foo". The goal is not to make a compiler that produces machine code or eventually gets a package manager, at all. They're not playing that game. They are writing a type system, not a language. (Note the title.) They're attempting to write one that captures the very weak guarantees of concurrent systems, and this is actually really complicated, so research tends to start with a simple version of the new type system, and then steadily narrow the assumptions behind it over subsequent publications. The target is not machine code, but having a computer check your typing rules work and that you can write interesting proofs with it. The toy language only exists for this purpose. The same way a Haskell programmer might code until it compiles and then put it into production, a PL researcher codes until the Coq checker gets all the way through their proofs and then submits to the conference. And much the same way that you can implement a GHC extension to test an idea, Coq is an extremely feature-rich base to start building a type checker demo language and proof system. They are not wasting any time here. The syntax they end up with is not meant to be used, it is meant to be the smallest possible language that demonstrates the theory in a machine-checkable way. If you want these features in a real language, take the OCaml type checker they wrote and go write it again for that new C++ frontend Circle or something, this time accounting for all the wild requirements that pop up in a real compiler.

cormacrelf 3y ago

You seem to be implying these researchers are reinventing the wheel by making a syntax that isn't based on anything that's already implemented (like Haskell). That couldn't be further from it. The syntax is absolutely unimportant to a paper like this. Choosing to use curly braces is their version of naming a variable "foo". The goal is not to make a compiler that produces machine code or eventually gets a package manager, at all. They're not playing that game. They are writing a type system, not a language. (Note the title.) They're attempting to write one that captures the very weak guarantees of concurrent systems, and this is actually really complicated, so research tends to start with a simple version of the new type system, and then steadily narrow the assumptions behind it over subsequent publications. The target is not machine code, but having a computer check your typing rules work and that you can write interesting proofs with it. The toy language only exists for this purpose. The same way a Haskell programmer might code until it compiles and then put it into production, a PL researcher codes until the Coq checker gets all the way through their proofs and then submits to the conference. And much the same way that you can implement a GHC extension to test an idea, Coq is an extremely feature-rich base to start building a type checker demo language and proof system. They are not wasting any time here. The syntax they end up with is not meant to be used, it is meant to be the smallest possible language that demonstrates the theory in a machine-checkable way. If you want these features in a real language, take the OCaml type checker they wrote and go write it again for that new C++ frontend Circle or something, this time accounting for all the wild requirements that pop up in a real compiler.