Re: Formal modeling of systems based on E/CapTP/(Water)Ken/Cap'n Proto ideas

Tony
It was done this way using capability addressing in the hardware instructions of computers like PP250. Very effective IMHO. 
That was prior to the crushing impact of the microprocessor. 
k

Sent from my iPhone

> On Jul 6, 2015, at 14:04, Tony Arcieri <[email protected]> wrote:
> 
> One thing I've observed about distributed object capability systems is that things like handling errors and ensuring messages don't get dropped is generally described in terms of "guidelines". I'm thinking things like COVR here.
> 
> This gives a developer a lot of expressiveness and flexibility, but not a lot of assurances that making a single misstep anywhere will break everything.
> 
> Tools like temporal logic (with mechanically checked proofs) and (formally modeled) replicated state machines seem like they could help here, and ensure that all potential failure modes are handled in some way (even if it's surfacing an error). I'm thinking of something like TLA+ here, at least to model check an approach like COVR.
> 
> Have there been any attempts at applying temporal logic to proving the correctness of object capability systems?
> 
> -- 
> Tony Arcieri
> _______________________________________________
> cap-talk mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk