prydt

Something I'm curious about: How does a recovering node know that it is healthy enough to serve requests? Is there some anti-entropy protocol used between the tail and the recovering node?

Is this still true today? I know that Facebook does [1], but I don't have references for any other places which use it.

Refinement types can be used as compile time checks for preconditions and postconditions, while this contract programming is inserting runtime checks.

The correct way to go about this would be to return the new balance and capture the return value in the first part of the out postcondition like:

```D double deposit(double amount) in (amount > 0, "Deposit amount must be positive") out (result; result == balance) { balance += amount; return balance; } ```

My mistake!