aseipp

OK and the vast majority of people excluding you and them probably have a very close-or-nearly-identical idea about what should happen. So everyone can be happy, there's nothing being lost here.

You'll live.

FoundationDB development has not stalled; v8 is still on the way. If anything, it's mostly just been stable for a while now, and it has now been developed as open source longer than it existed as closed source.

> Hardware performance is more important than software performance if the algorithm is likely to be implemented in hardware

I don't think that's necessarily a given at all, but I grant that's mostly a matter of opinion I guess.

> Given that the purpose of the competition was to replace SHA2 if/when it is weakened

I think the dirty secret hiding there is that I see very few actual expectations SHA2 will ever be broken. Assuming it can be and picking a different secure construction, of course, is a good idea. But even the designers of BLAKE have admitted such and so did NIST.

Performance is an evolving target. Meta reported they spend ~0.05% (1 out of every 2000 CPU cycles) on X25519 key exchange within the last year, which is quite significant. If that can be brought down, that's worthwhile. And ongoing research and deployment of PQC will make key exchange even more expensive.

> If there is not some novel, brand new algorithm that is being employed, the answer is because it is insecure.

Lol that is just not true at all. A major point of discussion when NIST announced the SHA3 finalist being Keccak back in ~2012(?) was that BLAKE1 at the time offered significantly better software performance, which was considered an important practical reality, and was faster than SHA-2 at a higher (but insignificantly so) security margin; their own report admitted as much. The BLAKE1 family is still considered secure today, its internal HAIFA design is very close to existing known designs like Merkle–Damgård, it isn't some radically new thing.

So why did they pick Keccak? Because they figured that SHA-2 was plenty good and already deployed widely, so "SHA-2 but a little faster" was not as compelling as a standard that complimented it in hardware; they also liked Keccak's unique sponge design that was new and novel at the time and allowed AEAD, domain separation, etc. They admit ultimately any finalist including BLAKE would have been a good pick. You can go read all of this yourself. The Keccak team even has new work on more performant sponge-inspired designs, such as their work on Farfalle and deck functions.

The reality is that some standards are chosen for a bunch of reasons and performance is only one of them, though very important. But there's plenty of room for non-standard things, too.

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.