Aether: High-performance, formally-verified storage engine written in Rust
1–10 of 15 posts
Re: Aether: High-performance, formally-verified storage engine written in Rust
#2It's so hard to trust a vibe coded software with something with a thing as valuable as data.
I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite.
Sorry mate.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#3It's so hard to trust a vibe coded software with something with a thing as valuable as data. I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite. Sorry mate.
Formal verification should catch vibe coding bugs.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#4big words, either you are a genius, or it's AI slop and we'd be better off using write(). Don't think there's inbetween.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#5It's so hard to trust a vibe coded software with something with a thing as valuable as data. I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite. Sorry mate.
Formal verification should catch vibe coding bugs.
The part that’s not clear to me is, does the spec actually align with what’s been implemented, or has the spec only been formally verified. I think the risk with vibe coding this sort of thing is that claude assures you the rust code implements the spec when it doesn’t
Re: Aether: High-performance, formally-verified storage engine written in Rust
#6It's so hard to trust a vibe coded software with something with a thing as valuable as data. I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite. Sorry mate.
Formal verification should catch vibe coding bugs.
This is the entire formal verification effort, as far as I can tell:
https://codeberg.org/gregburd/aether/src/branch/main/aether/...
They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system.
Any formal verification is of course awesome to see though.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#7Earlier quoted context omitted.
Formal verification should catch vibe coding bugs.
This is the entire formal verification effort, as far as I can tell: https://codeberg.org/gregburd/aether/src/branch/main/aether/... They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system. Any formal verification is of course awesome to see though.
I have to admit I used to think any level of formal verification was worthwhile.
But I recently tried having agents try starting with formal models, and then building code using that as basis. In the end to models were never detailed enough to catch the most common issues that were shaken out with getting a high level of coverage and mutation testing.
At which point, the predictive power of the formal models became somewhat vacuous.
I’m trying to be more optimistic that maybe using dependently typed languages will yield better results.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#8I don't think formally verifying my showing that the model is correct is good enough anymore. You must prove that your implementation refines the model.
Re: Aether: High-performance, formally-verified storage engine written in Rust
#9It's so hard to trust a vibe coded software with something with a thing as valuable as data. I see no reason why would anyone even bother checking this out, while there a trusted, battle scared, and non vibe-coded alternatives such as postgres, duckdb,boltdb,SQLite. Sorry mate.
Yeah it seems pretty insane to use a vibe-coded storage engine unless you had no other option
Re: Aether: High-performance, formally-verified storage engine written in Rust
#10The rest of the comments, as of now, are unreasonably unsubstantiated and a little bit hostile. AFAICS it's a large effort combining some pretty damn cool ideas from database internals world - this must have been written by someone experienced. It reminded me of RocksDB immediately, and wanted to see the example of integration, but then I saw redis, memcached, and "financial" database workload/protocol implementations. Good stuff, especially the benchmarks.
The code was obviously written using LLMs and I don't say this because the code looks like it's been LLM-generated but because of the fact that no sane person would have been able to write such complex piece of software in the pre-AI era. To me personally it shows how things dramatically shifted in software, and how domain expertise along with the AI became not 10x but 100x multiplier.