MaxBarraclough

Linus doesn't agree. He once said in an interview that making Linux GPL'd was definitely the best thing I ever did, [0] and has said that I love GPLv2. I really think the license has been one of the defining factors in the success of Linux because it enforced that you have to give back. [1]

That's not correct. Gforth features a JIT compiler, although they don't call it that, they call it dynamic superinstructions. It will be enabled if you run gforth-fast. If I understand correctly, the native code sequences are always generated at runtime, and cannot be baked into an image file.

In Forth's defence, other languages also have tricky subtleties, e.g. C++. Neither language prioritises theoretical purity, of course. They would be very different languages, with different drawbacks and advantages, if they did.

Both papers touch on whether the behaviours of certain unusual Forth constructs are well-defined according to the ANS Forth language standard. This sort of discussion should be quite familiar to C++ programmers.

A 12% difference in performance between two compilers, for some given application, is possible even between two of the best optimising compilers available. A 12% performance lag does not necessarily relegate a compiler to obscurity.

The long-entrenched MSVC compiler is still a major player despite that, for at least some applications and for at least some compiler versions, Clang outperforms it by far more than 12%. [0][1]

If a new Rust compiler really could offer significantly fewer compiler bugs, that would of course need to be weighed against any performance penalty, and the proper tradeoff would of course depend on the project.

> I agree that this is an impressive feat. I also don't see why an equivalent for rust would be adopted.

I imagine it wouldn't be widely adopted for most applications. CompCert itself is pretty niche. It's not Free and Open Source software, which I suspect is a factor, alongside its technical drawbacks.

Unless you're working on ultra-low-defect software, such as in a safety-critical domain, compiler bugs are unlikely to be a major factor in your software's quality. If the compiler lacks support for interesting language features, it becomes an even harder sell for 'ordinary' projects that are able to tolerate an ordinary number of compiler bugs.

I wouldn't say so. The gap between GCC and Clang/LLVM is bigger than that on some benchmarks, [0] although the gap between their overall performance (using geometric mean) is much less. [1]

It's a very impressive result considering how much effort has gone into GCC. It highlights how compiler optimisation work can face diminishing returns.

> the norm for releases being O2 if I understand correctly

Agreed, but the difference isn't that great. From the article:

> CompCert code is 7% slower than gcc-01 and 12% slower than gcc-02 on average.

Reminds me of how the cproc/qbe C compiler gets very roughly 50% of the performance of Clang/LLVM in 0.1% the lines-of-code. [2]

This 2022 article [0] says it generates binaries that run about 7% slower than what GCC produces with -O1.