joshlk

Some of the Lean proofs are 50k lines - is that normal?

What's a good reference to learn about Wavelet Matrices?

Asking a silly question… what piece of kernel code do you find the most awe-inspiring or impressive?

The top claim is that it's "Incredibly Fast" but I can't find any performance benchmarks. Can anyone find a link?

R-Trees are a good data structure to use in this case, enabling you to query a collection of intervals for overlap with another in O(log(n)) time.

Wikipedia: https://en.wikipedia.org/wiki/R-tree

Yes

Rust can be used in an embedded environment and also offers asynchronous execution built into the language

What your describing is social Darwinism, an argument used by fascist.

> [numpy] stores everything in rows

This isn't true. Pandas uses Numpy to store columns of data. Theres quite a few technical errors in the article.

What do you do in the summer when the homes don’t want the heat?

When using low precision formats like float8 you usually have to upscale the activations to BF16 before normalising. So the normalisation layers are proportionally using more compute when going to lower precision. Replacing these layers would help reduce the compute cost significantly.

It measures the proportion of questions for that language out of all languages. So, if there is a general decline in Stackoverflow questions, it’s already accounted for in the metric

According to Stackoverflow trends, Julia’s popularity is decreasing and very small

https://trends.stackoverflow.co/?tags=julia

Can you use to launch an Intel VM on Apple Silicone and visa versa? I’m interested in doing this so I can compile C++ applications for different architectures on MacOS. Do you know of any other “easy” methods?

Other than bandwidth, is there any other performance differences between Cloudflare and GitHub Pages?

Tensors used in deep learning are not the same as the definition used by Physicists - blame the DL community for this :). So DL tensors are just N-dimensional arrays of data, and there is no concept of covariance and contravariance of the dimensions. You could think of DL tensors as Cartesian tensors and they don't need to conform to the same transformation laws that Physics tensors do.

Warp is great - I use it as my daily terminal. The best features are being able to edit commands, chunking the output into blocks and AI generated commands at your fingertips.

Would it be possible to move all the language developers to work on packaging?

IMO the Python language is feature complete but the packaging system needs heart surgery.

I’m not sure this holds as true if it’s the same team creating both implementations.

I found the advertisements the most interesting bit

> I have never met a scientist who can resist the lure of fast-but-dangerous math

This made me chuckle

Is this analogous to the Python 2 to 3 jump?

Why the large jump from Java 8 to 17?

That was fun.

On another note, I dislike how “Zero-Knowledge Proofs” are called proofs. It’s not a proof. You iteratively increase your belief that the result is true, like in experimentation, but that’s not a proof.

I now use GitHub pages to host websites and it works like a charm. Free hosting and you can edit the pages using the GitHube website

Is there an explanation of the acronyms/metrics used? E.g. COP

I’m sure it’s down to use case and circumstances but I frequently find it useful to be able to read and edit text based data formats (JSON/YAML/TOML). If you are concerned about data size you can easily use on-the-fly compression at little cost nowadays.

Side question: when did XML start to loose favour to JSON? Did this happen because of something in particular or was it a gradual transition?

Because it hurts EU customers by not applying the rules worldwide.

If Apple maintains that it will only support new web engines in the EU, the EU will step in and force Apple to allow it worldwide. So it's a losing battle for them.