I only skimmed the page and it looks like a really cool idea, but I have a question about this:
types to let you express things like “the Client communicates this to Service, then Service communicates that to the Login Provider, then […]”
If the client needs to know about all that stuff that happens after its call to Service, isn't Service a leaky abstraction? My idea of OO, which I got from GOOS[1], is that each object talks only to its neighbors and it shouldn't have to know about their neighbors' neighbors or their neighbors' implementation details because the messages sent between objects are at the level of the domain. Same with microservices, in principle. The benefit is that you can reason about each object/microservice in isolation. If you must know that A then B then C then D, why split the code/services in the first place?Sorry if the docs already answer this, I'll have a closer look later.
That's wishful OO thinking.
It's led to Mockito-style testing (some people call it 'unit', others call it 'integration'). You decide that the behaviour of file.read() is that it returns a string of its contents. You judge your software correct on the basis of how it processes the returned string. Then you launch, and in the real world, the behaviour of file.read() is to return a FileHandleNotOpen exception, so you fix your code, improve your mocks to cover the opening/closing scenario, and re-release it. Next time you run it, it throws a FileNotFound exception. So you fix your code, then extend your mocks to cover that scenario too. Later still, you call read() twice in prod, and hit a FileHandleAlreadyClosed exception (apparently the first read closed the file for you). Fix the mocks again.
You wanted Mockito to lead reality, but it lags it. Rather than Mockito being a useful tool to get your prod system working well, your prod system is actually a useful tool to get your Mockito mocks working well.
Choreographic programming lets you specify this protocol in one place. "The file will be opened, the file will be read, the file will be closed, etc." Then the different parties can't guess/assume or come up with their own half of the protocol incorrectly.