[HN Gopher] Conformance Checking at MongoDB: Testing That Our Co...
___________________________________________________________________
Conformance Checking at MongoDB: Testing That Our Code Matches Our
TLA+ Specs
Author : todsacerdoti
Score : 18 points
Date : 2025-06-02 21:50 UTC (1 hours ago)
(HTM) web link (www.mongodb.com)
(TXT) w3m dump (www.mongodb.com)
| usernamed7 wrote:
| There's a paragraph that literally starts with "system."
|
| > system. It's too complex and detailed, so it's not much easier
| to understand than the implementation code, and state-space
| explosion dooms model checking. The author abandons the spec and
| concludes that TLA+ is impractical. In the eXtreme Modelling
| style, a big system is modeled by a collection of small specs,
| each focusing on an aspect of the whole. This was the direction
| MongoDB was already going, and it seemed right to me.
|
| This reads like AI generated slop. Which is actually on brand,
| because Mongo is slop.
| compton93 wrote:
| I consulted on a project that was using MongoDB even though it
| was obvious from the concept that an RDBMS would be better,
| however I went in with an open mind and gave MongoDB a red hot
| crack. It straight up ignored indexes with no explainable
| reason why. We had a support contract and they just gave us the
| run around.
___________________________________________________________________
(page generated 2025-06-02 23:00 UTC)