aseipp

It says they intend the backend to be used for FEC, so it's probably an untimed model that it outputs. Sail would probably generate bad SystemVerilog anyway even if it was timed/synthesizable because the language doesn't have any concepts to express things like pipelining or the necessary concurrency primitives or properly structured modules for the output netlists.

If you want a high-level RTL with some of the dependent features of Sail, but for hardware that can generate good SystemVerilog, I think Bluespec is probably the best complement.

Anthropic or Google offering a product and having margins they leverage is not "lock in" when there are dozens of alternatives at many various price points, including ones that can be run entirely locally (at high capex cost). It's like market fact #0 that, today, there is very little moat here other than capital, which is why OpenAI has now got multiple viable competitors despite their head start. Their APIs get copied, their tools get copied, the only way they remain competitive is with huge investments back into the core product to retain their leads. This is just what a competitive market looks like right now, and these offerings exist exactly because of downward pressure from other forces. The goal is of course to squeeze other players as much as possible, but these products have not yet proven to be sticky enough for their mere existence to do that. And there are many other players who have a lot of incentive to keep that downward pressure applied.

What you're describing is really just called "Offering a product for sale" and yes typically the people doing it will do, say, and offer things that encourage using their product over the competitors. That isn't "lock in" in any sense of the word. What are they supposed to do? Say "Our shit sucks and isn't price effective compared to others and we bring nothing to the table?" while giving you stuff for free?

Companies that are putting down millions for fab runs absolutely pay shitloads of money for it. The cost of design and verification of those components is enormous and that's mostly what you pay for. People have been shipping Andes and SiFive IP for years now. Downloading source dumps for C910 cores is not the hard part.

For most places that kind of high-cost work doesn't make much sense when their product isn't "a CPU", and they also typically have to buy other IP anyway like memory controllers or I/O blocks -- so buying a CPU core isn't that strange in the grand scheme.

It does not look like it due to its largest target audience (hardcore math nerds writing proofs), but Lean 4 is actually a meta-programming language, like Racket -- it is one single unified language for programming, meta programming, and theorem proving, on top of a small core. The implementation of Lean is almost entirely written in Lean, including components like LSP servers, the compiler itself, many efficient data structures, etc. It is a key use case to write real world programs, because the implementation itself is such a program.

In the long past, Lean 3 had this idea that you could use one language both for writing proofs, and writing proof automation -- programs that manipulate proofs and automatically do things. Like in the article itself, the 'grind' thing-a-mabob is proof automation. (Roqc has two separate languages for proofs and proof automation.) But there was a problem: Lean started as a theorem prover and the implementation tried to move towards "executing programs" and it didn't work very well and was slow. The prototype compiler from Lean 3 to C++ ran out of steam before Lean 3 got canned.

Lean 4 instead went and did things the other way around: it started as a programming language that was executable. The Lean 4 compiler was self-hosted during development for a long-time, way before anyone ported any big math proofs to it from Lean 3. Why did they do this? Because the key insight is that if you want to write programs that manipulate proofs (AKA programs), the best thing to have at hand is have a robust general programming language -- like Lisp or Racket. And so Lean is macro based, too, and like Racket it allows you to have families of languages and towers of macros that expand as deep as you want. Meta programs that write programs that write programs, etc...

So in Lean you write Lean programs that can manipulate Lean ASTs, and you write "reader macros" that allow you to use domain specific syntax right inside the source file for any kind of math or programming-language DSL you want. And all those macros and meta-programs are compiled and executed efficiently just like you'd expect. Finally, there is a total fragment of the language that you can actually write proofs over and reason about. And there is a big library called "mathlib" with lots of macros for writing math and math proofs in this language-framgent-we-can-reason-and-prove-things-with.

Lean 4 is very close in spirit to the Lisp idea, but modified for math proving and generalized programming. It's very unique and powerful.

Nice list of solid changes. I really like Deno for scripting random glue code; I use it most places (maybe with the exception of random machine learning stuff, where python/uv fits.) Looking forward to gRPC support later this year, too, for some of my long-tail use cases. And the bundle command looks nice!

The performance is great, and now there's a fully stable userspace graphics driver stack. Peripherials basically work. The battery life under load (i.e. development) is serviceable, not terrible, but in my (limited, "I turn on my laptop after some amount of time" testing) it's not even close to macOS especially when turned off. This is with a 13" M2 Air.

It's a really good Linux laptop if you can find a M2 somewhere, IMO.

There already is ROCm support for PyTorch. Then there's stuff like this: https://semianalysis.com/2024/12/22/mi300x-vs-h100-vs-h200-b...

They have improved since that article, by a decent amount from my understanding. But by now, it isn't enough to have "a backend". The historical efforts have spoiled that narrative so badly that it won't be enough to just have a pytorch-rocm pypi package; some of that flak is unfair though not completely unsubstantiated. But frankly they need to deliver better software, across all their offerings, for multiple successive generations before the bad optics around their software stack will start fading. Their competitors are already on their next gen architecture since that article was written.

You are correct that people don't really invoke CUDA APIs much, but that's partially because those APIs actually work and deliver good performance, so things can actually be built on top of them.

The Top500 is an irrelevant comparison; of course AMD is going to give direct support to single institutions that give them hundreds of millions of dollars and help make their products work acceptably. They would be dead if they didn't. Nvidia also does the same thing to their major clients, and yet they still make their products actually work day 1 on consumer products, too.

Nvidia of course has a shitload more money, and they've been doing this for longer, but that's just life.

> smaller systems

El Capitan is estimated to cost around $700 million or something with like 50k deployed MI300 GPUs. xAI's Colossus cluster alone is estimated to be north of $2 billion with over 100k GPUs, and that's one of ~dozens of deployed clusters Nvidia has developed in the past 5 years. AI is a vastly bigger market in every dimension, from profits to deployments.

Ah, that clears it up a bit. Thanks! Looking forward to all of this. (For the interested readers, here's the SSE library: https://github.com/janestreet/ocaml_simd/tree/with-extension...)

Your comment remains completely stupid regardless of how much of it is in the quote. OxCaml's goal is to be upstreamed. "I don't see the point in this unless people have programs using OCaml" and it's like, yeah, that's the point of adding features to a computer program. Any computer program. Because people already use the computer program and it will be useful to them.

FWIW, the "Get OxCaml" page actually says that SIMD on ARM isn't supported yet. If it actually works it would be worth removing that from the known issues list https://oxcaml.org/get-oxcaml/

Yeah, pretty excited about this one even though it seems minor. A paper and talk by the author of this particular feature from ML2024, too:

- https://www.youtube.com/watch?v=WM7ZVne8eQE

- https://tyconmismatch.com/papers/ml2024_labeled_tuples.pdf

> Not seeing much of a point in this

OCaml is a good language and these extensions are very welcome to existing OCaml programmers and programs, as well as many of the other extensions Jane Street has added. I don't understand what you mean here.

Yes, they've used this terminology for a while, even the recent technical paper on this effort was titled "Oxidizing OCaml with Modal Memory Management", though the word "oxidize" itself is never actually referenced or defined in the paper. A bit strange, I agree, though it's kind of catchy I admit.

The tailscale client is not proprietary.

To be clear, Jujutsu is not "porcelain" in the (somewhat archaic) Git sense of "high level tools built on low level tools". We do not share any code with the git project. Jujutsu uses Git as a storage layer, i.e. the direct on disk representation. The algorithms and user interface are all completely written from scratch, on top of this.

You could also write e.g. a Mercurial backend to Jujutsu and it would operate similarly, but using revlog storage vs Git's content addressed store.

> JJ uses the git binary

That's a relatively recent phenomenon. The git binary is used only to fetch and push objects. Previously we used libgit2. Why do this? Because replicating all of git and OpenSSH's feature support for every little random auth flow/crypto algorithm/hardware token/whatever is a battle that can't be won. It's ultimately smarter to just have an uglier interface between the two parts (invoking a command line vs using an API) to make the end-user experience significantly better.

When working with Git objects, jj uses the Gitoxide rust library to natively manage the Git store and upstream Git is not used at all.

Yes, that's basically the relationship between CoVE and ACE, from a quick glance. In this case, ACE is simply implementing a formally modeled and verified security monitor where the design has been extracted to Coq and the invariants proven.

It can work on P550 because CoVE supports several "Deployment strategies", the one ACE uses is referenced in the README: CoVE spec, Appendix D, "M-mode [Trusted Security Manager] based deployment model" https://github.com/riscv-non-isa/riscv-ap-tee/blob/main/src/... -- the other appendicies detail e.g. Smmtt based designs, and apparently there's a not-yet-written "Nested Virtualization" design in Appendix C.

They also note that the P550 isn't a "true" port due to the preliminary, non-ratified H extension, and it also misses another required extension called "Sstc" but they just emulate it. (Sstc is interesting; it seems to be a performance optimization for delivering timer interrupts directly to supervisors, but I can imagine in the case of CoVE timer interrupts going through M-mode could leak data, making it more of a security issue.)

Leveraging M-mode is basically how previous security monitors like keystone worked too, back on the original HiFive Unleashed. It just sorta treats M-mode as an analogue to the "secure world" in ARM parlance, though there is no requirement that M-mode has e.g. an encrypted memory controller and dedicated memory region, and I'm guessing other things (I'm not super familiar with TrustZone.)

Broadly speaking this reminds me as a kind of a evolution/combination of Microsoft's Komodo (formally verified, but was only for e.g. SGX-style enclaves) and existing M-mode TEE systems like Keystone -- but upgraded to support "Confidental Computing" virtual machines. So that's quite nice.

There is a fork of Mesa with some support for the onboard GPU (Immortals G720), but it's not upstream yet and might not be for a while. Some people on the forums have installed various discrete GPUs, which would obviously work (modulo bugs.)

There is also an open source driver for the NPU somewhere (Zhouyi NPU) and some documentation, but nothing in an upstream kernel yet. https://zhouyi-npu-tutorial.readthedocs.io/en/latest/0_radxa...

The size of the vector width really isn't as important as the general design of the instructions themselves. It's pretty trivially easy to extend the number of lanes and vector width with the right design. This is separate from the problem of "what is the best size for the particular host machine I'm running on", but that's something we've already been handling in various ways for a while, without needing wholly new instruction set designs.

"In a fantasy land that doesn't exist, or maybe last existed decades ago, this wouldn't be needed." OK, that's nice. What does that have to do with reality as it stands today, though?

> Is this a fair comparison?

Is this a serious question? Orion uses WebKit which practically speaking is like 80% of what people know as "a browser" and where an insane amount of the effort and money goes. There are like 30 various WebKit-derived zero-features 1-man browsers out there on GitHub, they even show up here sometimes. Firefox maintains its own entire engine called Gecko, it's completely incomparable. The actual development cost of your browser is subsidized almost entirely by Apple (and Kagi's VC money), make no mistake about it.

Haskell's "mixin modules" AKA backpack are I think the closest thing you're going to get outside of SML (they are a different trade off in the design space, it's not 1-to-1), but they have languished in the broader community due to a couple social factors. They are excellent for many of the same things you use modules for, though, and work just fine in my experience.

On the same note, the lack of some kind of module system along these lines (broadly all defined in terms of "holes" in a compilation unit which are "plugged up" later on at instantiation time), is one of my biggest complaints about Rust. The extensive usage of traits in the broader ecosystem results in this phenomenon (identical to Haskell) where global coherence requires your dependency tree gets tied up in the location of types and their trait impls. In other words, you cannot abstract over your dependencies in a truly modular way.

Global coherence requirements are fine (preferable even!) for many things but if it's the only hammer you have, well, you know the rest of the metaphor.

> Anyway I think there is a proposal for it so it'll probably work its way in eventually.

Modular implicits have been shelved indefinitely from what I understand, if that's what you're referring to.

OCaml's syntax is not what's "holding it back" in my personal opinion, but that doesn't mean it's "fine". I regularly praise it as a language (even as a former developer of the main Haskell compiler, which adopted Mixin-style modules decades after the fact) and "the syntax looks like shit" is absolutely one of the first immediate turn-offs for pretty much everyone I talk to. It's also one of my own complaints, but OCaml has a lot of good stuff too so I can put up with it.

When I was working on GHC many years ago OSUOSL helped us by providing us access to some nice POWER7 machines (courtesy of an IBM kernel hacker who recommended and endorsed us) and we used them for years to solve weird issues. I've always thought very highly of the Open Source Lab. I hope someone can help them make it through this.

https://eprint.iacr.org/2017/536.pdf is the relevant paper that introduces the project and its broad design. Figure 1 on page 3 is a good place to look.

I mean, most if not all of the code they're replacing (e.g. the vendored and vectorized Blake2 code) is also going to be designed and optimized with timing attacks in mind and implemented to avoid them. CVE-2022-37454 was literally found in a component that was optimized and had timing attack resistance in mind (XKCP from the SHA-3 authors). "Code that is already known to be wrong" is not really a meaningful baseline to compare against.

The goal is to make things safer, yes, but speed is absolutely a major priority for the project and a requirement for production deployment, because the difference in speed for optimized designs vs naive ones might be an order of magnitude or more. It's quite speedy IME. To be fair to your point, though, it's also a moving target; "which is faster" can change as improvements trickle in. Maybe "shouldn't be much slower" is a better statement, but I was speaking generally :)

(You could also make the argument that if previous implementations that were replaced were insecure that their relative performance is ultimately irrelevant, but I'm ignoring that since it hinges on a known unknown.)

It isn't boasting about anything, it's a straightforward description of the 2.5 years of effort they went through for this project, and some of the more annoying "production integration" bits.

Extreme ELI5 TL;DR: Your Python programs using the cpython interpreter and its built in cryptographic modules will now be using safer and faster, with no need for you to do anything.

> The primary purpose of HTTP2 was to allow servers to preemptively push files/resources to clients to avoid round-trip latency; to reduce the reliance on script bundles.

No, it was not. The primary goal of HTTP/2 was to get over traditional connection limits through connection multiplexing because browsers treat TCP connections as an extremely scarce resource. Multiplexing massively improves the ability to issue many asynchronous calls, which are very common -- and H2 went on to make the traditional HTTP stack more efficient across the board (i.e. header compression.) Some of the original HTTP/2 demo sites that popped up after Google first supported it in Chrome were of loading many images over HTTP/1 vs HTTP/2, which is very common. In one case of my own (fetching lots of small < 1kb files recursively from S3, outside the browser) HTTP/2 was like a 100x performance boost over HTTP/1 or something.

You're correct Server Push was tacked on and known to be flawed very early on, and it took a while before everyone pulled the plug on it, but people fixated on it because it just seemed really cool, from what I can tell. But it was never the lynchpin of the thing, just a (failed and experimental) boondoggle.