n_u

> The total number of concurrent requests represents the number of simultaneous requests moving through the pipeline at any point in time. Unlike a GPU batch, those requests don’t wait for one another to finish, they stream through the pipeline continuously.

What do they mean by “unlike a GPU batch”? It’s not a hardware limitation of GPUs right? It’s just the scaffolding to do this in software isn’t available right

My first question was “How do they know the proof correctly corresponds to the software they are checking?”

They say “ While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are: The formal models of RISC-V and of Linux processes;

The exact theorem statements that were proved;

The Rocq proof checker itself.”

What are the formal models of RISCV and Linux? I’m guessing they allow translation of RISCV code directly into Rocq proofs?

I’d love to see more info about their workflow of code -> proof. Or even an open source tool

This is really cool! Go is so dead simple to learn but it just lacks a few features. I feel this really fills that specific gap.

Go with more expressive types and a bit stricter compiler to prevent footguns would be a killer backend language. Similar to what TypeScript was to JavaScript.

My 2 cents would be to make it work well with TypeScript frontends. I think TypeScript is so popular in backends because 1. you can share types between frontend code and backend code and 2. it's easy for frontend devs to make changes to backend code.

I think they mean they would prefer more rigorous statistical analysis.

"Rigor cleans the window through which intuition shines" - Ellis Cooper

I've found it's ok at Rust. I think a lot of existing Rust code is high quality and also the stricter Rust compiler enforces that the output of the LLM is somewhat reasonable.

Good article! Small suggestions:

1. It would be nice to define terms like RSI or at least link to a definition.

2. I found the graph difficult to read. It's a computer font that is made to look hand-drawn and it's a bit low resolution. With some googling I'm guessing the words in parentheses are the clouds the model is running on. You could make that a bit more clear.

One big difference is that with unwrap in Rust, if there is an error, your program will panic. Whereas in Go if you use the data without checking the err, your program will miss the error and will use garbage data. Fail fast vs fail silently.

But I'm just explaining the argument as I understand it to the commenter who asked. I'm not saying it is right. They have tradeoffs and perhaps you prefer Go's tradeoffs.

I think the argument is that the compiler does not enforce that the error must be checked. It's just a convention. Because you know Go, you know it's convention for the second return value to be an error. But if you don't know Go, it's just an underscore.

In a language like Rust, if the return type is `Result<MyDataType, MyErrorType>`, the caller cannot access the `MyDataType` without using some code that acknowledges there might be an error (match, if let, unwrap etc.). It literally won't compile.