> Do you mean the type checker that runs during compiling connects to the database? Okay, it doesn't go that far. But the compiler produces the table creation

> Do you mean the type checker that runs during compiling connects to the database? Okay, it doesn't go that far. But the compiler produces the table creation scripts. So, if your build process includes running said scripts, then database and application types are guaranteed to be synchronized. > Do you have a sample code of these table invariants at hand? I'd gladly take a look... Imagine a general ledger that's guaranteed to never go out of balance, no matter what third party modules do that interact with the accounting subsystem, because the only module that can directly manipulate accounting tables is the accounting subsystem. Guaranteed by the type checker. I haven't implemented such a thing in Ur/Web, because implementing accounting systems from scratch is a frigging lot of work, most of it utterly boring, and nobody has paid me to do it. But it's feasible, and the ML module system is the reason why.