Comment by win311fwg

> Suppose I have a User with some attributes like birthday, email and whether they have been verified.

Philosophically, birthday and email are not attributes of a user. If you remove a user from existence, a birthdate and email address still exist. So...

> would you create UserWithBirthdayAndEmail type

...yes, something like a `profile { user, birthday, email }` type is necessary to compose the attributes you are interested in into something where those attributes do belong together.

> it feels like it is going to bloat the interface space, how do you tackle this problem?

Like all things formal verification, increase the level of verification in your critical sections and don't sweat the non-critical sections. How impactful will it be to your business if sending a birthday email message fails?