gz09
Joined 13 years ago
Karma
363
Submissions
80
Member since
Dec 4
Recent submissions
Comment · 1 month ago
Comment · 1 month ago
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.
Comment · 3 months ago
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).
Comment · 6 months ago
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.
Comment · 7 months ago
> 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.
Comment · 7 months ago
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.
Comment · 8 months ago
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...
Comment · 8 months ago
Yep pretty much, feldera is the engine we don't control what SQL people throw at us.
Comment · 8 months ago
> 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.
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.