Proof-driven programming

wakuwaku describes itself as a proof-driven microservice framework. The idea is simple: every property of a service should be proven by the tool that is best at proving it, as early as possible. In practice that means correctness is split in two halves.

Macro correctness: the compiler proves the wiringCopy Anchor Link

In wakuwaku, "how things fit together" is expressed as trait bounds. A bound is a proposition, and an impl that satisfies it is the proof. The trait solver either finds the proof or the program does not build.

Take the ServiceBuilder. Registering a cron job that is built from a SessionStore requires the bound

ServiceBuilder<Head, Chain>: ProvideAt<SessionStore, Position>

which reads "somewhere in this builder, at some position, a SessionStore is registered". The builder is a list at the type level, so the compiler can check that statement. There is no runtime map, no Any, no downcasting, and therefore no startup panic for a missing dependency: the mistake never reaches a binary.

If you come from Spring, compare this with the application context. Spring resolves beans when the context starts, so a missing bean is reported when the application boots (NoSuchBeanDefinitionException). wakuwaku performs the same check while compiling, so it is reported by cargo build, by your editor, and by CI, before anything is deployed.

The same technique is used across the crates: capabilities on data access handles, algebra markers on events, and proof types for validated values all turn a class of runtime bugs into type errors. The catalogue below lists them.

Micro correctness: unit tests prove the behaviorCopy Anchor Link

Types can say that a job has a SessionStore; they cannot say that it deletes the right sessions. That is what tests are for, and wakuwaku is designed so that those tests are cheap to write.

Every component is a plain Rust value. It is created from its dependency with ServiceCreation::create_service, or composed from several services with the compose_* methods, and its behavior is a single async method:

• a cron job is a Processor of CronTicks;
• an event handler implements EventHandler::handle, which has the same shape;
• a gRPC service implements the trait generated by tonic;
• a data access handle (Db) is a Processor of queries;
• a predicate is checked with prove, a pure check with its PureVerifier.

A test creates the value and calls the method. No Iggy server, no open port, no scheduler. The Testing page shows a test for each kind of component.

The Processor abstractionCopy Anchor Link

The common shape comes from the kanau crate, which wakuwaku re-exports as wakuwaku::deps::kanau:

pub trait Processor<I: Send> {
    type Output;
    type Error;

    fn process(&self, input: I) -> impl Future<Output = Result<Self::Output, Self::Error>> + Send;
}

A processor is a stateful async function: the struct holds the dependencies, and process turns an input into a result. You implement it with a plain async fn:

impl Processor<CronTick> for ExpireSessions {
    type Output = ();
    type Error = std::convert::Infallible;
    async fn process(&self, tick: CronTick) -> Result<(), Self::Error> {
        let removed = self.sessions.remove_expired(tick.fired_at);
        tracing::info!(removed, "expired sessions");
        Ok(())
    }
}

If you know tower::Service, the differences are deliberate:

Taking &self is what lets the framework run one value from many places at once: a consumer processes several keys of a batch concurrently with the same handler (wrapped in an Arc), and a test can call the same value twice. The returned future must be Send, so components can run on Tokio's multi-threaded runtime.

Processor composes, too. The write hooks of wakuwaku::entity are processors that wrap another processor of the same queries, so a hooked handle is a drop-in replacement for the plain one.

What the compiler rejectsCopy Anchor Link

Each row below is a mistake that does not build. Follow the link for the full explanation.

Four of them, with the real compiler output (paths and help notes trimmed):

A dependency that was never registeredCopy Anchor Link

let (_services, cron) = ServiceBuilder::new(Mailer) // no SessionStore registered
    .cron_job::<ExpireSessions, _>()
    .start();

error[E0277]: the trait bound `(): ProvideAt<SessionStore, _>` is not satisfied
   |
37 |         .cron_job::<ExpireSessions, _>()
   |          ^^^^^^^^ the trait `ProvideAt<SessionStore, _>` is not implemented for `()`
   |
   = note: required for `ServiceBuilder<Mailer>` to implement `ProvideAt<SessionStore, There<_>>`
note: required by a bound in `ServiceBuilder::<Head, Chain>::cron_job`

() is the end of the list: the compiler searched every registered service and did not find a SessionStore.

A write through a read-only handleCopy Anchor Link

async fn on_replica(db: &Db<Memory, ReadOnly>) {
    db.process(DeletePost(1)).await.unwrap();
}

error[E0277]: the trait bound `ReadOnly: Covers<Write<Post>>` is not satisfied
   |
32 |     db.process(DeletePost(1)).await.unwrap();
   |        ^^^^^^^ the trait `CanWrite<Post>` is not implemented for `ReadOnly`
   |
   = note: required for `ReadOnly` to implement `Covers<Write<Post>>`
   = note: required for `Db<Memory, ReadOnly>` to implement `Processor<DeletePost>`

An unvalidated valueCopy Anchor Link

fn rename(name: Proven<String, NonEmpty>) -> String {
    name.subject().clone()
}

fn main() {
    let name = String::from("Ann");
    rename(name);
}

error[E0308]: mismatched types
   |
27 |     rename(name);
   |     ------ ^^^^ expected `Proven<String, NonEmpty>`, found `String`

A cron job with no intervalCopy Anchor Link

impl CronJob for Busy {
    const INTERVAL: CronJobInterval = CronJobInterval::AtLeast(Duration::ZERO);
}

let (_services, cron) = ServiceBuilder::new(SessionStore).cron_job::<Busy, _>().start();

error[E0080]: evaluation panicked: CronJob::INTERVAL must not be zero
note: the above error was encountered while instantiating `fn CronRegisterCenter::<Busy>::new`

What the types do not proveCopy Anchor Link

Being precise about the limits matters as much as the guarantees:

• External state. Whether the Iggy topic exists, whether a configured partition exists, and whether two handlers share an event type tag are checked when the consumer starts, not when it compiles. Two gRPC servers with the same service name make the router panic when the servers are added.
• What a query really does. A capability proves routing: code wired to a Db<_, ReadOnly> never issues a query declared as a write. It cannot prove that a query declared as a read does not write, so keep the database's own guard on replicas.
• The moment of a proof. A Proven value records that a predicate held when it was checked. If the predicate depends on a database row, the row may have changed since.
• Business logic. That is micro correctness, and it is the job of your tests.