Proof types in Dart: Using final classes as computational witnesses

# Proof types in Dart: Using final classes as computational witnesses Source: [https://modulovalue.com/blog/proof-types-in-dart/](https://modulovalue.com/blog/proof-types-in-dart/) Here is a pattern that Dart 3\.0 made possible: ``` final class EmailValidated { const EmailValidated._(); } EmailValidated? validateEmail(String email) { if (_isValidEmail(email)) { return const EmailValidated._(); } return null; } ``` If you have an instance of`EmailValidated`, the validation must have occurred\. Nothing outside this library can produce an`EmailValidated`without going through`validateEmail`\. The type system enforces it\. I call these proof types\. Others call them witness types or evidence types\. Whatever the name, the idea is the same: the existence of a value proves that a computation happened\. ## Table of Contents - [Why This Works](https://modulovalue.com/blog/proof-types-in-dart/#why-this-works) - [A More Complete Example](https://modulovalue.com/blog/proof-types-in-dart/#a-more-complete-example) - [Carrying Data with Proofs](https://modulovalue.com/blog/proof-types-in-dart/#carrying-data-with-proofs) - [Authorization Checks](https://modulovalue.com/blog/proof-types-in-dart/#authorization-checks) - [What About Other Languages?](https://modulovalue.com/blog/proof-types-in-dart/#what-about-other-languages) - [Parse, Don't Validate](https://modulovalue.com/blog/proof-types-in-dart/#parse-dont-validate) - [The Curry\-Howard Correspondence](https://modulovalue.com/blog/proof-types-in-dart/#the-curry-howard-correspondence) - [When to Use Proof Types](https://modulovalue.com/blog/proof-types-in-dart/#when-to-use-proof-types) - [Limitations](https://modulovalue.com/blog/proof-types-in-dart/#limitations) - [Conclusion](https://modulovalue.com/blog/proof-types-in-dart/#conclusion) - [Addendum](https://modulovalue.com/blog/proof-types-in-dart/#addendum) ## Why This Works Four things combine to make this possible: 1. `final`prevents the class from being extended, implemented, or mixed in outside its library \([see my post on class modifiers](https://modulovalue.com/blog/understanding-dart-class-modifiers-lattices/)\) 2. A library\-private constructor \(`\.\_\(\)`\) prevents instantiation outside the library 3. Dart's library\-based privacy means these restrictions are absolute, not advisory 4. A sound type system \(both static and dynamic\) ensures types cannot be forged\. Dart's unsound constructs \(like`as`casts\) fail loudly at runtime rather than silently producing invalid values\. You cannot accidentally end up with a fake`EmailValidated`\. The*only*way to obtain an`EmailValidated`instance, then, is to call`validateEmail\(\)`with an input that passes validation\. ## A More Complete Example Let's build a user registration system where the type system enforces that all checks have passed: ``` // registration_proofs.dart /// Proof that an email address has been validated. final class EmailChecked { final String email; const EmailChecked._(this.email); } /// Proof that a password meets strength requirements. final class PasswordChecked { const PasswordChecked._(); } /// Proof that the terms of service were accepted. final class TermsAccepted { const TermsAccepted._(); } /// Proof that all registration requirements have been met. final class RegistrationReady { final String email; const RegistrationReady._(this.email); } EmailChecked? checkEmail(String email) { final regex = RegExp(r'^[^@]+@[^@]+\.[^@]+$'); if (regex.hasMatch(email)) { return EmailChecked._(email); } return null; } PasswordChecked? checkPassword(String password) { if (password.length >= 12) { return const PasswordChecked._(); } return null; } TermsAccepted? checkTermsAccepted(bool accepted) { if (accepted) { return const TermsAccepted._(); } return null; } RegistrationReady? prepareRegistration( EmailChecked email, PasswordChecked password, TermsAccepted terms, ) { // All checks have provably passed. We can trust these values. return RegistrationReady._(email.email); } ``` Now the registration function: ``` // registration_service.dart import 'registration_proofs.dart'; void register(RegistrationReady proof) { // This function CANNOT be called unless: // 1. Email was validated // 2. Password was checked // 3. Terms were accepted // // The compiler enforces this. Documentation and code review cannot. createAccount(proof.email); } ``` The caller cannot construct a`RegistrationReady`instance directly\. They must go through`prepareRegistration\(\)`, which requires the three proof types, which can only be obtained by passing the respective checks\. ## Carrying Data with Proofs Proof types can carry validated data: ``` final class ParsedInt { final int value; const ParsedInt._(this.value); } ParsedInt? parseInt(String input) { final result = int.tryParse(input); if (result != null) { return ParsedInt._(result); } return null; } ``` Now`ParsedInt`is both a proof that parsing succeeded and a carrier for the parsed value\. This pattern works well for authorization: ``` final class Authorized<T> { final T resource; const Authorized._(this.resource); } Authorized<Document>? authorizeDocumentAccess( User user, Document document, ) { if (user.canAccess(document)) { return Authorized._(document); } return null; } void deleteDocument(Authorized<Document> proof) { // The authorization check provably happened. // No need to check again. proof.resource.delete(); } ``` ## What About Other Languages? This pattern requires the ability to create types that cannot be instantiated outside their defining module\. Let's see which languages support this\. ### JavaScript JavaScript has no mechanism for this\. Classes can always be instantiated: ``` class Validated { #private = true; // Private field, but... constructor() {} // Constructor is always accessible } // Anyone can do this: new Validated(); ``` Even with private fields, you cannot prevent construction\. The language simply doesn't have the concept of a sealed type\. ### TypeScript TypeScript's type system is erased at runtime\. Private constructors exist but provide no runtime guarantees: ``` class Validated { private constructor() {} static create(): Validated { return new Validated(); } } // TypeScript prevents this at compile time: // new Validated(); // Error // But at runtime, it's just JavaScript: // Anyone with access to the transpiled code can bypass this ``` More fundamentally, TypeScript uses structural typing\. Any object with the right shape satisfies an interface: ``` interface Validated { readonly _brand: unique symbol; } // You can still create objects that match: const fake = { _brand: Symbol() } as Validated; ``` Branded types are a workaround, but they're not enforced\. They rely on developers not bypassing them\. ### Python Python's philosophy is "we're all consenting adults\." Nothing is truly private: ``` class Validated: def __init__(self): pass # "Private" by convention only class _Validated: def __init__(self): pass # Anyone can still do: _Validated() # Works fine ``` Even with`\_\_slots\_\_`, metaclasses, or`\_\_new\_\_`tricks, determined code can always create instances\. ### Java Java has`final`classes and private constructors: ``` public final class Validated { private Validated() {} public static Validated create() { return new Validated(); } } ``` This looks promising, but Java has reflection: ``` Constructor<Validated> constructor = Validated.class.getDeclaredConstructor(); constructor.setAccessible(true); // Bypass private Validated fake = constructor.newInstance(); // Creates instance ``` The`setAccessible\(true\)`call bypasses all access control\. Unless you run with a restrictive SecurityManager \(which almost no one does, and which is deprecated since Java 17\), private constructors provide no guarantee\. ### Kotlin, Scala, C\#, and PHP The same story repeats across these languages\. Kotlin and Scala run on the JVM and inherit its reflection, C\# has \.NET reflection, and PHP has its own Reflection API\. In every case, the equivalent of Java's`setAccessible\(true\)`forces access to a private constructor, so the guarantee is advisory rather than enforced\. ### Go Go's unexported types \(lowercase names\) can only be used within their package: ``` package validation type validated struct { value string } func Validate(input string) *validated { if isValid(input) { return &validated{value: input} } return nil } ``` This actually works for the basic case\. External packages cannot create`validated`instances directly\. However, Go's type system has limitations\. Interfaces are structural, not nominal, and the`unsafe`package can bypass protections\. It's closer to what we want but not as clean as Dart's approach\. ### C C has no classes, but you can use opaque pointers: declare a struct in a header without defining it, and only expose functions that return pointers to it\. External code cannot allocate the struct directly\. However, C's lack of type safety means you can cast anything to anything\. One`memcpy`or pointer cast and your guarantees evaporate\. ### C\+\+ C\+\+ has`final`classes \(since C\+\+11\) and private constructors\. Unlike Java, C\+\+ has no runtime reflection that can bypass access control\. However,`friend`declarations punch holes in encapsulation, and pointer arithmetic or`reinterpret\_cast`can forge any type\. If you trust your codebase not to do unsafe things, C\+\+ can approximate proof types, but the language doesn't enforce it\. ### Ruby Ruby is dynamic and open by design\. Classes can be reopened, methods redefined, and`send`can call private methods\. Nothing is truly sealed\. ### Swift Swift can achieve this pattern: ``` public final class Validated { fileprivate init() {} } public func validate() -> Validated? { // Only this file can create Validated return Validated() } ``` With`final`preventing subclassing and`fileprivate`/`private`preventing construction, Swift provides similar guarantees to Dart\. Swift's reflection \(Mirror\) is read\-only, but`unsafeBitCast`can still forge an instance out of arbitrary bits\. As in Rust, that requires deliberately reaching for an explicitly unsafe API\. ### Rust Rust handles this through its module system: ``` mod validation { pub struct Validated { value: String, // private field } impl Validated { pub fn new(input: &str) -> Option<Validated> { if is_valid(input) { Some(Validated { value: input.to_string() }) } else { None } } } } // Outside the module, you cannot construct Validated // because you cannot access the private field ``` Rust's module system and private fields make this pattern natural\. The one escape hatch is`unsafe`:`std::mem::transmute`or`std::mem::zeroed`can fabricate a value with private fields\. But that means writing the word`unsafe`, a loud, greppable signal that ordinary code never uses\. ### Haskell Haskell pioneered many of these ideas\. ``` module Validation (Validated, validate) where newtype Validated = Validated String validate :: String -> Maybe Validated validate input | isValid input = Just (Validated input) | otherwise = Nothing ``` By not exporting the`Validated`constructor, external code cannot create values of that type\. This pattern has been used in Haskell for decades\. The one loophole is`unsafeCoerce`, which can manufacture a`Validated`from anything\. Like Rust's`unsafe`and Swift's`unsafeBitCast`, it is an explicit, unmistakable escape hatch, not something normal code stumbles into\. ### OCaml [gasche pointed out](https://www.reddit.com/r/ProgrammingLanguages/comments/1uyv0pv/comment/oy56gyq/)that OCaml, from the ML family with a richer module system than Haskell's, offers two ways to do this\. The first mirrors the Haskell approach: keep the type abstract in the module signature\. ``` module Email : sig type validated val validate : string -> validated option val to_string : validated -> string end = struct type validated = string let validate s = if is_valid_email s then Some s else None let to_string s = s end ``` Inside the module`validated`is just a`string`, but the signature hides that\. Outside code needs`Email\.to\_string`to read the payload and has no way to construct a`validated`on its own\. The second has no Dart equivalent: a private type abbreviation\. ``` module Email : sig type validated = private string val validate : string -> validated option end = struct type validated = string let validate s = if is_valid_email s then Some s else None end ``` Here`validated`is a one\-way subtype of`string`\. You can coerce a`validated`down to a`string`with`\(x :\> string\)`and read the payload for free, but you cannot go the other way, so the only way to obtain a`validated`is through`validate`\. It is the same guarantee with less ceremony than a fully abstract type\. Both are undone only by`Obj\.magic`, OCaml's`unsafeCoerce`\. It casts any value to any type and skips the constructor entirely, so as in the other languages here, forging a proof takes that one explicit, unsafe step\. ### Summary LanguageProof Types Possible?Why / Why NotJavaScriptNoNo access control on constructionTypeScriptNoTypes erased, structural typingPythonNoEverything accessible, dynamic typingJavaNoReflection bypasses privateKotlinNoJVM reflection bypasses privateC\#NoReflection bypasses privateGoPartiallyUnexported works, but`unsafe`existsCNoPointer casts bypass everythingC\+\+PartiallyNo reflection, but`friend`and casts existScalaNoJVM reflection bypasses privateRubyNoDynamic, classes can be reopenedPHPNoReflection bypasses privateSwiftYesfinal \+ private init, no bypassing reflectionRustYesPrivate fields, strong module systemHaskellYesModule exports control constructionOCamlYesAbstract or private types control constructionDartYesfinal \+ private constructor, mirrors deprecated and disabledDart sits alongside Swift, Rust, Haskell, and OCaml in providing this capability\. Dart does have reflection, through`dart:mirrors`, but mirrors are deprecated, disabled by default in Flutter, and unavailable when compiling to JavaScript\. For all practical purposes, Dart code cannot bypass private constructors\. One honest caveat: the "Yes" languages are not truly airtight\. Each has a deliberately unsafe escape hatch, Rust's`transmute`, Swift's`unsafeBitCast`, Haskell's`unsafeCoerce`, OCaml's`Obj\.magic`, and Dart's disabled`dart:mirrors`\. The distinction from the "No" languages is not that forging is impossible, but that it requires explicitly invoking an unsafe operation rather than ordinary reflection or normal typed code\. What makes Dart notable is that it's a mainstream, accessible language that runs everywhere \(web, mobile, desktop, server\) while still providing these guarantees\. You don't need to learn a systems language or a functional language to use proof types\. ## Parse, Don't Validate Proof types embody the principle of["parse, don't validate"](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/)\. Validation checks if data is valid and returns a boolean or throws an exception\. The data keeps its original type: ``` bool isValidEmail(String email) { return RegExp(r'^[^@]+@[^@]+\.[^@]+$').hasMatch(email); } void processEmail(String email) { if (!isValidEmail(email)) { throw ArgumentError('Invalid email'); } // email is still just a String // Nothing stops you from passing an unvalidated string here } ``` The problem: you can forget to call the validator, or call it and ignore the result, or pass an unvalidated string to a function expecting a validated one\. The type system doesn't help\. Parsing transforms data into a new type that encodes validity in the type itself: ``` final class ValidEmail { final String value; const ValidEmail._(this.value); } ValidEmail? parseEmail(String email) { if (RegExp(r'^[^@]+@[^@]+\.[^@]+$').hasMatch(email)) { return ValidEmail._(email); } return null; } void processEmail(ValidEmail email) { // Can only be called with a ValidEmail // Which can only be obtained by successfully parsing } ``` Now the type system enforces that`processEmail`only receives validated emails\. You cannot forget to validate because the types won't match\. You cannot pass raw strings because the compiler rejects them\. Proof types take this further\. They need not carry any data at all\. The value's existence alone certifies that a computation occurred\. ## The Curry\-Howard Correspondence The pattern in this post rests on a well\-known result from theoretical computer science: the[Curry\-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)\. The correspondence states: - Types are propositions - Programs are proofs - A value of a type is a proof of that proposition When you declare`final class EmailValidated`, you're declaring a proposition: "this email was validated\." When you have a value of type`EmailValidated`, you have a proof of that proposition\. If a type has no public constructor, the only way to obtain a proof is through the functions that construct it\. The function`validateEmail`is the only way to prove the proposition`EmailValidated`\. And that function only produces a proof when validation actually succeeds\. In languages with more expressive type systems \(like Agda, Coq, or Idris\), you can encode complex propositions and have the compiler verify sophisticated invariants\. Dart's type system is simpler \(for a good reason, one I might discuss in the future\), but the core principle applies: if you control construction, you control what can be proven\. ## When to Use Proof Types Proof types are useful when: 1. Security\-critical checks must have occurred \(authorization, rate limiting\) 2. Validation must be enforced before processing 3. Multi\-step processes require all steps to complete 4. APIs should make invalid states unrepresentable 5. Machine\-generated or third\-party code must not be able to skip a required check They're overkill when: 1. The check is trivial and always passes 2. Performance is critical and the extra objects matter 3. The codebase is small and single\-author ## Limitations Proof types have some limitations to keep in mind: Library scope: The guarantee holds only outside the library\. Within the library that defines the proof type, any code can construct instances\. Keep proof\-generating logic focused and correct\. No temporal claims: A proof type proves the check happened, not when\. If state can change between obtaining the proof and using it, you may need to revalidate\. For example, an`Authorized`proof obtained before a permission change might be stale\. No subject binding:[tsanderdev pointed out](https://www.reddit.com/r/ProgrammingLanguages/comments/1uyv0pv/comment/oy2bcf1/)that an empty proof like`PasswordChecked`is weak on its own\. Such an instance proves only that some password was validated somewhere over the app's lifetime, not that this user's password was validated for this request\. A proof that carries no data is ambient, so any`PasswordChecked`is interchangeable with any other\. This is a fair point, and the password example does not survive it cleanly\. Passwords are unbounded, and Dart cannot put values into its type system, so "a proof for exactly this password" is not something the compiler can express\. That example cannot be made fully safe at compile time, and a better one would carry a bounded, identifiable subject\. You can still make the pattern safer at runtime by storing a username or a session token inside the proof and checking it where the proof is consumed, so a mismatched or reused proof fails at runtime even though the type system will not catch it for you\. This is also the motivation for phantom types, a related technique I want to cover in a future post\. More generally, generics can bind a proof to a type, the way`Authorized<Document\>`does, but not to a specific value such as one particular user id, because Dart has no dependent types\. Runtime cost: Each proof is an object allocation\. For hot paths, consider whether the safety benefit justifies the cost\. Extension types are a middle ground here: free at runtime and safer than a bare value, though as the[addendum](https://modulovalue.com/blog/proof-types-in-dart/#extension-types-are-not-a-replacement)explains, they can be forged, so they are not a true proof\. ## Conclusion [Dart 3\.0's class modifiers](https://modulovalue.com/blog/understanding-dart-class-modifiers-lattices/)enabled a pattern that many mainstream languages cannot express\. By combining`final`with library\-private constructors, you can create types whose mere existence proves that computations occurred\. The type system stops being just a way to catch typos\. It becomes a tool for encoding your program's invariants and protocols directly\. When you see a function that takes a`RegistrationReady`parameter, you know, without reading the implementation or the documentation, that all registration checks have passed\. The types tell you\. This is the kind of capability that makes me excited about Dart's evolution: a small addition to the type system, and suddenly you can encode guarantees that used to require a much fancier language\. **PS:**Of the four languages that support proof types, only Dart aims to have an efficient type system\. Rust's macro system is Turing\-complete\. Swift's type system can express unbounded computation \(someone[implemented Brainfuck in Swift's type system](https://forums.swift.org/t/brainf-in-the-swift-type-system/68301)\)\. Haskell's type\-level programming can loop forever\. Once a type system can run arbitrary computation, type checking has no upper bound on how long it can take\. The other three languages have all crossed that line\. Dart has not, and it shows in practice: Haskell, Rust, and Swift are all notorious for slow compile times\. Rust's own[2025 compiler performance survey](https://blog.rust-lang.org/2025/09/10/rust-compiler-performance-survey-2025-results/)found slow compilation to be the single most\-cited pain point, and roughly 45% of respondents who had abandoned Rust listed long compile times as one of their reasons\. Swift ships a dedicated error,["expression was too complex to be solved in reasonable time"](https://danielchasehooper.com/posts/why-swift-is-slow/), for expressions whose overload resolution blows up exponentially\. And in Haskell circles,[complaining about compile times](https://www.parsonsmatt.org/2019/11/27/keeping_compilation_fast.html)is practically a rite of passage\. Dart gives you proof types without the compile\-time tax\. That advantage is deliberate\. A[2010 Google memo](https://gist.github.com/paulmillr/1208618)that made the original case for building Dart listed the "Ability to be Tooled" as one of its three core goals, a design constraint JavaScript's structure could never satisfy\. Tooling friendliness, it seems, has been a guiding star for Dart from the very beginning, and that heritage is a large part of why it stands apart from the other proof\-type languages here\. **PPS:**Everything above assumes a[closed world](https://en.wikipedia.org/wiki/Closed-world_assumption)\. When your Dart code runs in the VM or is compiled to native code, this assumption holds\. When compiled to JavaScript, things get murkier\. JavaScript runtimes support all kinds of shenanigans \(prototype manipulation,`eval`, dynamic property access\) that could potentially let adversarial code violate these guarantees\. If you're defending against malicious code running in the same JS context, proof types alone won't save you\. If you need these guarantees on the web,[WebAssembly](https://dart.dev/web/wasm)closes the gap: Dart compiles to WASM, which runs in a sandboxed linear\-memory model with none of those escape hatches, so the closed\-world assumption holds there too\. --- [Discuss on r/dartlang](https://www.reddit.com/r/dartlang/comments/1uydmcw/proof_types_in_dart_using_final_classes_as/) [Discuss on r/ProgrammingLanguages](https://www.reddit.com/r/ProgrammingLanguages/comments/1uyv0pv/proof_types_in_dart_using_final_classes_as/) --- ## Addendum ### Extension types are not a replacement [cent\-met\-een\-vin suggested](https://www.reddit.com/r/dartlang/comments/1uydmcw/comment/oxyzafk/)that Dart's extension types could express the same idea\. Extension types are a good middle ground: they give you essentially free performance and improved safety guarantees, but we can actually fake them\. An extension type is a compile\-time\-only view over a representation type\. At runtime, a value of an extension type is its representation, with no separate identity and no enforced construction\. Take an email proof written as an extension type: ``` extension type EmailValidated._(String value) { static EmailValidated? validate(String input) => _isValidEmail(input) ? EmailValidated._(input) : null; } ``` The private constructor looks like it guards construction, but extension types are erased to their representation at runtime\. Any string can be cast straight into one: ``` final Object raw = "definitely not an email"; final forged = raw as EmailValidated; // succeeds ``` Because`EmailValidated`erases to`String`, the check behind that cast is really`raw is String`, so it passes, and you get a "validated" email that was never validated\. This is the same weakness as TypeScript's branded types: a static\-only wrapper with no runtime guarantee\. A proof type needs a real class with a real library\-private constructor, precisely so that no cast can conjure one\. ### Sealed classes make proof types even more powerful [pavanpodila pointed out](https://www.reddit.com/r/dartlang/comments/1uydmcw/comment/oy0i10k/)that sealed classes push this technique further, and that is exactly right\. A`sealed`root lets you model a proof that is one of several known cases, and you get exhaustiveness checking in`switch`for free, so the compiler forces you to handle every branch\. ``` // A proof that a user's identity was verified, and how. sealed class IdentityVerified { const IdentityVerified._(); } final class VerifiedByEmail extends IdentityVerified { const VerifiedByEmail._() : super._(); } final class VerifiedByPhone extends IdentityVerified { const VerifiedByPhone._() : super._(); } ``` A function can then demand proof that verification happened and still react to how, with the compiler checking that every case is covered: ``` void grantAccess(IdentityVerified proof) { switch (proof) { case VerifiedByEmail(): print('verified by email'); case VerifiedByPhone(): print('verified by phone'); } } ``` Two details matter when you do this: - Each branch must be`final`, so that no outside code can subclass a branch to forge one\. - The root itself does not need`final`\. Marking it`sealed`already prevents extension outside its library, so it is implicitly closed\. This becomes much less verbose once[primary constructors](https://github.com/dart-lang/language/blob/main/accepted/3.13/primary-constructors/feature-specification.md)land, as[Comun4 noted](https://www.reddit.com/r/dartlang/comments/1uydmcw/comment/oxyyyqd/)\. Today each proof carries a small amount of constructor boilerplate, and primary constructors collapse most of it\. ### The library is the trusted core [EggplantExtra4946 asked](https://www.reddit.com/r/ProgrammingLanguages/comments/1uyv0pv/comment/oy2gs4v/): what stops a function in the same library from returning an`EmailValidated`without validating anything? ``` EmailValidated newEmail(String email) { return const EmailValidated._(); } ``` Nothing stops it, and that is by design\. Dart's privacy is library\-scoped\. A Dart library is a single compilation unit, not the folder of files that many other languages call a library\. The library that declares a proof type is its trusted core: code outside it is held to the guarantee, and code inside it is trusted to mint proofs correctly\. It is the author's job to keep that library small and its minting logic correct\. ### Backdoors Because the library mints its own proofs, a proof is only as trustworthy as the code that produces it\. A malicious or careless proof library can hand out valid proofs without doing the work: ``` EmailValidated? validateEmail(String email) { // Backdoor: this exact input is always accepted, even though it is not a valid email. if (email == "malicious") { return const EmailValidated._(); } if (_isValidEmail(email)) { return const EmailValidated._(); } return null; } ``` Every`EmailValidated`this returns is a real, unforgeable value of the type, so the compiler and every downstream caller trust it completely\. But`malicious`is not even an email, and it still gets one\. Proof types defend against a caller accidentally skipping a check\. They do not defend against the author of the proof library, who sits inside the trust boundary and can define "validated" however they like\. If you depend on someone else's proof types, you are trusting their minting code the same way you trust any dependency, so treat that code as security\-critical and keep it small enough to audit\. ### The email regex is both unsound and incomplete [RandalSchwartz noted](https://www.reddit.com/r/dartlang/comments/1uydmcw/comment/oy7nqug/)that the`checkEmail`regex,`^\[^@\]\+@\[^@\]\+\\\.\[^@\]\+$`, is far too naive to recognize[the actual email grammar](https://www.rfc-editor.org/rfc/rfc5322), and that a syntactically correct email regex is[famously thousands of characters long](http://www.ex-parrot.com/~pdw/Mail-RFC822-Address.html)\. The regex is wrong in both directions\. It is unsound, because it accepts strings that are not valid addresses:`John Doe@example\.com`passes, even though an unquoted space in the local part is not allowed\. It is also incomplete, because it rejects strings that are valid:`"John@Doe"@example\.com`is a legal address with a quoted local part, but the regex sees two`@`characters and gives up\. So an`EmailChecked`minted this way both over\-promises and under\-delivers\. This is the trusted\-core problem again, without any malice\. The type guarantees that`checkEmail`produced the value\. It cannot guarantee that`checkEmail`correctly captures "valid email", and here it does not\. As RandalSchwartz suggests, the fix is to mint the proof from a real grammar\-based parser\. Subscribe to get new posts\.