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

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)
  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.

Authorization Checks

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. We use it here as the representative for functional languages. OCaml, F#, and other ML-family languages have the same capability.

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.

Summary

Language Proof Types Possible? Why / Why Not
JavaScript No No access control on construction
TypeScript No Types erased, structural typing
Python No Everything accessible, dynamic typing
Java No Reflection bypasses private
Kotlin No JVM reflection bypasses private
C# No Reflection bypasses private
Go Partially Unexported works, but unsafe exists
C No Pointer casts bypass everything
C++ Partially No reflection, but friend and casts exist
Scala No JVM reflection bypasses private
Ruby No Dynamic, classes can be reopened
PHP No Reflection bypasses private
Swift Yes final + private init, no bypassing reflection
Rust Yes Private fields, strong module system
Haskell Yes Module exports control construction
Dart Yes final + private constructor, mirrors deprecated and disabled

Dart sits alongside Swift, Rust, and Haskell 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, 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".

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.

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.

Runtime cost: Each proof is an object allocation. For hot paths, consider whether the safety benefit justifies the cost.

Conclusion

Dart 3.0's class modifiers 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). 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 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", for expressions whose overload resolution blows up exponentially. And in Haskell circles, complaining about compile times is practically a rite of passage. Dart gives you proof types without the compile-time tax. That advantage is deliberate. A 2010 Google memo 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. 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 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.