xuejie

Just provide a not-related-at-all but IMHO still interesting case: I used to have a Kioxia CM6 U2 SSD drive, it would pass all sorts of benchmarks the reseller is willing to run, but whenever I tried to clean-compile Rust on it, the drive would fail almost certainly somewhere in the build process. While there are configurations you can compile Rust using pre-built LLVM, in my tests I'm compiling LLVM along the way. So I can agree with the comment here, there might be some unique property when doing multi-core compilations, though my tests show a potentially faulty drive, while the above comment here is about Intel CPU.

Like other comments here, just want to say thank you for this amazing editor! It has been my primary code editor for the past few years. I did use a few different editors for specific purposes(vscode for interactively proving coq code, joe/nvi for editing super large files), but micro does provide what I need in 90% of the cases :P

> The Raspberry Pi 4 is THE cheapest 2Gflops/W computer ever made and probably that will ever be made in the future too!

Can you expand on this one? I was curious why you think there probably will not be a cheaper one in the future with similar or better specs.

IMO such a category existed for quite a long time, JVM and .NET all falls into this category. Yes WASM has its fame for becoming a browser standard, but fundamentally, there is very little difference between WASM and JVM.

Personally, I already pulled the trigger 2 years ago when I first starting to write Rust professionally. A laptop just becomes far tooooo noisy compiling Rust code. These days I use 3 machines:

* A fanless Chromebook with decent screen for travel use

* An Intel NUC that is hooked to a big monitor, which is also the device I'm typing this on

* A beefy Ryzen desktop that sits in the corner of my balcony, which I usually connect via ssh and perform all the heavy tasks

To me I'm getting all the benefits of each computer, and the combined cost is still less than a so-called macbook pro :)

> I feel like the plethora of (partially incompatible) extensions make the language very complicated and messy. There is no single Haskell. Each file can be GHC Haskell with OverloadedStrings or GADTs or ....

Aren't macros, especially proc macros these days in Rust having the same effect? Personally I feel like this is a tradeoff every language has to play with: you either limit to a special way of writing, or adding some sort of ad-hoc system that enables rewriting syntax and even to a degree, semantics.

Thanks guys for the explanation! I truly have misunderstood this post.

The author first goes with:

> Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference.

But latter they also go on to say:

> Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.

I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also possible, is that a new language and a new runtime could enable new optimizations that are not possible before. The author did mention Chez's profiling tools help a lot in the rewrite. So I was curious: is it really true, that we cannot attribute some part of the speedup to language differences?

Also I was interested in the rationale behind using Scheme to replace Haskell, but I failed to find some reasoning behind this, anyone can shed some light on this?