fovc

Not sure I follow the analogy, so apologies if I'm reading it backwards, but we do in fact have standards for "good enough" brakes without being brake-maxxers.

Similarly here, I'd argue that a verified implementation with correctness proofs, mechanical translation, and easily auditable theorems seems close to good enough? A lot rides on the Claude-built translator, I suppose, but the trusted code for that project seems to be tiny in comparison to what it would have been 2 years ago!

sel4's guarantees break if you have DMA, e.g., from your NIC. It doesn't help with timing attacks. It doesn't cover your network stack. AFAIK, no one has taken up the mantle from Project Everest, so you'll need to write a verified TLS library. Once you've built all that, you can start thinking about your database/application/whatever. Then of course you'll have to verify all your dev's machines and scripts to ensure nobody is misusing a credential that can get stolen.

"So what?" you say. "Making a heavier-than-air metal tube take off and land millions of times per year without a catastrophe is also hard, and we no longer expect most or even many of those tubes to blow up or fall down."

Mother nature is not spending $$$ using AI and HI adversarially trying to find the exact combination of atoms that will cause your device to fail.

> I would always pick an incremental batch load with a cursor value over a CDC connection.

What's the benefit vs. something like Postgres's logical replication for CDC? IMO, the hard part of CDC is maintaining consistency in the face of potential network issues or downstream slowdowns. One is forced to choose between scylla: generate excess trx logs if replication slows, and charybdis: lose consistency. I don't see how an open transaction helps here?

> I also think it’s important to notice that a lot of these challenges they happen with humans too. The concept of prompt injection isn’t that different from social engineering, right? When somebody calls in and says, “Oh, I forgot my password, can you just help me this one time?”

Very nice! For other readers, vc is short for verification condition and wp is short for weakest precondition.

I wonder if the error propagation problem could be solved with a “branching” generator? Basically at every token you fork off N new streams, with some tree pruning policy to avoid exponential blowup. With a bit of bookkeeping you could make an attention mask to support the parallel streams in the same context sharing prefixes. Perhaps that would allow more of an e2e error minimization than the greedy generation algorithm in use today?

And also make sure that slot is a symbol in the correct package. Or do like Elisp and do without packages but then have a 16 character prefix