Extract JS observer

[jeapostrophe]

I think this is actually very easy. It is just a participant that does not actually participate (i.e. it does not send any messages.) Right now, this couldn't work though because we'd have to have an address for it that everyone else agrees on at the start of the protocol.

[jeapostrophe]

This pays attention the emit messages and displays games.

[fare]

Observability is more than a cute feature: it's an essential piece of infrastructure:

• It's how the interaction is visible by users, who can take appropriate actions (decide to sign messages indeed, decide whether or not the message is worth sending 3 couriers on different planes to ensure the message is posted before deadline despite a massive country-wide DDoS).
• It's how we can write interfaces that are logically separate from the program, so the program to prove remains small, while the interface is rich — using the back-program / fore-program pattern described in the last part of my thesis. That's part of the secret sauce that I believe enables us to prove programs correct that people not using our technique can never hope to because it's staggeringly complex for them.
• More generally, it's a crucial part of being able to make composable proofs across many layers of abstractions (which is the first part of my thesis).

[fare]

In practice, that's how we can write an interface that from the point of view of the proof system is a typed hole, yet allows the front-end programmer to use rich contextual data at source-level (or otherwise appropriate level of abstraction) in presenting the data to users.