Conformance checking at MongoDB: Testing that our code matches our TLA+ specs

Been an SRE and DBA for almost 20 years and the only truth in tech I firmly believe in: use whatever you want in a new project. Build fast and get it out. Once you have paying users, hire old dads like me to move you to Cassandra or Vitess or TiDB or something, or dont and just pay the bills for mongodb and laugh all the way to Series C.

I wouldn't start a new project with MongoDB, I'd probably use ScyllaDB, and i'd spent months getting the data model just right while you launch and get paying customers.

Personal opinion.

I swore away from it for 10 years, but came back recently. And I'm pleasantly surprised with the developer experience of MongoDB Atlas (the cloud version).

You just have to keep in mind the common sense best practices about developing with kv stores, and you'll be mostly alright.

Only here you read that MongoDB is a legacy product.

Fortnite runs on MongoDB, it's one of the largest game on the planet.

15 years ago Postgres did not have proper replication, shocking right?

> or are there still good reasons for using it in a new project in 2025

it's not clear there ever was. Most of the big users I'm aware of, like Stripe, don't seem to have needed it and regretted the decision. Big data didn't become a thing in the way people expected[0]. If you really did need the scalability of Mongo you'd choose a NewSql database like TiDB[1].

[0] https://motherduck.com/blog/big-data-is-dead/ [1] https://docs.pingcap.com/

MongoDB as a company is growing 20% y/y and 2B in revenue.

So very far from being a legacy product.

I still use it for new projects because (a) Atlas is genuinely a solid offering with a great price point for startups and (b) schema-less datastores have become more of a necessity as our control of data has decreased e.g. SaaS companies dictate their schema and we need to accomodate.

The original storage engine was terrible, but they wised up and later acquired and adopted WiredTiger as the default. It was sort of their InnoDB moment and went a long way to improving performance, reliability, replication, and other "enterprisey" features.

I think it’s just fairly rare that formal verification is valuable to a business.

Obviously all software benefits from correctness — but we all know that software certainly doesn’t need to be bug-free to make money!

And if the benefits of formal verification don’t outweigh the (non-trivial!) costs — and critically, outweigh them in a business-person-legibile way — then people won’t put up the time and effort.

Mike Dodds' article "What Works (and Doesn't) Selling Formal Methods" offers some insight - two points were: (i) many potential applications of formal methods in business do not result in an attractive cost-benefit outcome, relative to mainstream software development approaches, especially in being able to produce enough benefit for a small input of time / resources. (ii) anecdote: one business that needs to produce software that complies with certain validation/quality targets - say achieved with a baseline method using a lot of manual QA and without formal methods - does not get a business benefit to investing in increased validation, they just need enough enough validation to clear the compliance bar or rank slightly ahead of the competition. if formal methods could assist them in achieving the same level of validation to meet their compliance obligations with less cost than their baseline development and QA processes then they might have much more appetite to invest in formal methods.

https://www.galois.com/articles/what-works-and-doesnt-sellin...

corresponding HN thread from earlier this week: https://news.ycombinator.com/item?id=44131324

It's the complete opposite of asking an LLM to make an app, which is all the rage.

Honestly... Just like with writing extensive unit tests, you will then end up basically writing the program twice. Which is not going to appeal to the "move as fast as possible" crowd.