gz09

> A human, you can hold accountable, and you can keep them at a good security posture with short-lived session tokens.

You can do this too (and better) with a repo: OIDC/Workload identity trust relationship between github and aws for short lived tokens + a github environment setup that requires manual approval. Bonus: It also gives you an audit trail with a github action log as opposed to a sysadmin running something on a laptop.

The problem here was mostly that they (for some reason) happened to use (and leak) a PAT.

Results seem somewhat reasonable given that the amount of verus/TLA/Creusot/Lean code out there is tiny compared to all the other non-formal code.

So it's understandable that the agents wont be able to go beyond proving trival things, given how much more difficult it is to write such code.

A (more) interesting experiment (to me) would be to write a high level spec manually for a non-trivial system (liveness etc.) and see if the agent can produce an implementation using guided refinements that satisfies this specification.

Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done.

Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).

our CLAUDE.md / AGENTS.md specifically calls out good engineering books, which I think does help:

From https://github.com/feldera/feldera/blob/main/CLAUDE.md:

- Adhere to rules in "Code Complete" by Steve McConnell.

- Adhere to rules in "The Art of Readable Code" by Dustin Boswell & Trevor Foucher.

- Adhere to rules in "Bugs in Writing: A Guide to Debugging Your Prose" by Lyn Dupre.

- Adhere to rules in "The Elements of Style, Fourth Edition" by William Strunk Jr. & E. B. White

e.g., mentioning Elements of Style and Bugs in Writing certainly has helped our review LLM to make some great suggestions about English documentation PRs in the past.

> not one mention of the origin of the trick

And who or what would you say is the origin? The "trick" is so old I'm afraid it is lost to time to say who invented the bitmap. It was used in MULTICS or THE long before PostgreSQL was invented.

That would be surprising to me if anyone would think this is novel.

Using bitmaps to indicate whether things are in-use or not is very common in systems programming. Like you said PG does it, but most other systems do this too. It's not specific to databases: in an operating system, one of the first thing it needs is an allocator, the allocator most likely will use some bitmap trick somewhere to indicate what's free vs. what's available etc.

Haha, looks like it.

I remember the first time I encountered this thing called TPC-H back when I was a student. I thought "wow surely SQL can't get more complicated than that".

Turns out I was very wrong about that. So it's all about perspective.

We wrote another blog post about this topic a while ago; I find it much more impressive because this is about the actual queries some people are running: https://www.feldera.com/blog/can-your-incremental-compute-en...

Yep pretty much, feldera is the engine we don't control what SQL people throw at us.

> Isn't there still a way to express at least one Illegal string in ArchivedString?

There may be good reasons (I don't know any) why it wasn't done like this, but from a high-level it looks possible to me too yes.

Feldera is an incremental query engine, you can think of it as a specialized database. If you have a set of question you can express in SQL it will ingest all your data and build many sophisticated indexes for it (these get stored on disk). Whenever new data arrives feldera can instantly update the answers to all your questions. This is mostly useful when the data is much larger than what fits in memory because then the questions will be especially expensive to answer with a regular (batch) database.

Feel free to try it out, it's open source: https://github.com/feldera/feldera/

Yep, this comment sums it up well.

We have many large enterprises from wildly different domains use feldera and from what I can tell there is no correlation between the domain and the amount of columns. As fiddlerwoaroof says, it seems to be more a function of how mature/big the company is and how much time it had to 'accumulate things' in their data model. And there might be very good reasons to design things the way they did, it's very hard to question it without being a domain expert in their field, I wouldn't dare :).

> Depending on your needs, the right tool might be Parquet or Arrow or protobuf or Cap’n Proto

I think parquet and arrow are great formats, but ultimately they have to solve a similar problem that rkyv solves: for any given type that they support, what does the bit pattern look like in serialized form and in deserialized form (and how do I convert between the two).

However, it is useful to point out that parquet/arrow on top of that solve many more problems needed to store data 'at scale' than rkyv (it is just a serialization framework after all): well defined data and file format, backward compatibility, bloom filters, run length encoding, compression, indexes, interoperability between languages, etc. etc.

> it sounds like helping customers with databases full of red flags is their bread and butter

Yes that captures it well. Feldera is an incremental query engine. Loosely speaking: it computes answers to any of your SQL queries by doing work proportional to the incoming changes for your data (rather than the entire state of your database tables).

If you have queries that take hours to compute in a traditional database like Spark/PostgreSQL/Snowflake (because of their complexity, or data size) and you want to always have the most up-to-date answer for your queries, feldera will give you that answer 'instantly' whenever your data changes (after you've back-filled your existing dataset into it).

There is some more information about how it works under the hood here: https://docs.feldera.com/literature/papers

Point them to us https://github.com/feldera/feldera -- we are hiring ;)

Absolutely, it's a very common technique :)

I wasn't sure about writing the article in the first place because of that, but I figured it may be interesting anyways because I was kind of happy with how simple it was to write this optimization when it was all done (when I started out with the task I wasn't sure if it would be hard because of how our code is structured, the libraries we use etc.). I originally posted this in the rust community, and it seems people enjoyed the post.

Hi, I'm the author of the article.

As to your hard disagree, I guess it depends... While this particular user is on the higher end (in terms of columns), it's not our only user where column counts are huge. We see tables with 100+ columns on a fairly regular basis especially when dealing with larger enterprises.

Security models from SaaS companies based on having a bunch of random bytes/numbers with coarse-grained permissions, and valid for a very long time are already a bad idea. With agents, secrets/tokens really need to be minted with time-limited, scope-limited, OpenID/smart-contract based trust relationships so they will fare much better in this new world. Unfortunately, this is a struggle still for most major vendors (e.g., Github gh CLI still doesn't let you use Github Apps out-of-the box)

> It's pretty clear that the security models that were design into operating systems never truly considered networked systems

Andrew Tanenbaum developed the Amoeba operating system with those requirements in mind almost 40 years ago. There were plenty of others that did propose similar systems in the systems research community. It's not that we don't know how to do it just that the OS's that became mainstream didn't want to/need to/consider those requirements necessary/<insert any other potential reason I forgot>.

feldera has a way to run ad-hoc/list queries on materialized views. Alternatively, you can send the result somewhere where you can query it.

I believe that was more a bug in the firmware that's been fixed for a while now.

It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).

It does leverage various models, but

- github copilot PR reviews are subpar compared to what I've seen from other services: at least for our PRs they tend to be mostly an (expensive) grammar/spell-check

- given that it's github native you'd wish for a good integration with the platform but then when your org is behind a (github) IP whitelist things seem to break often

- network firewall for the agent doesn't seem to work properly

raised tickets for all these but given how well it works when it does, I might as well just migrate to another service