These are chat archives for jdubray/sam

21st
Mar 2017
Michael Terry
@formido
Mar 21 2017 03:57
Jean-Jacques Dubray
@jdubray
Mar 21 2017 04:01
@formido thank you so much for pointing this out
Edward Mulraney
@edmulraney
Mar 21 2017 08:46
@jdubray it would be interesting for you to create an article/blog about how SAM relates to TLA+
because from all my research into TLA+ I couldn't really see any major links between SAM and TLA+. It seems there were shared English terminology, but not actually principles/methodologies
Jean-Jacques Dubray
@jdubray
Mar 21 2017 11:27
@edmulraney It's kind of ironic you ask that question since:
1/ There were multiple threads on that topic in this forum and I pointed out very precisely the articulation
2/ I have tried to have this discussion with you back in December as to what is the definition of an action (Dr. Lamport defines is unequivocably) and it seems that our discussion has stalled
Jean-Jacques Dubray
@jdubray
Mar 21 2017 11:34
That being said, I gave this lecture last month on State Machines and Computation which hopefully had some precision to that question.
The slides explain:
1/ how state machines compute
2/ how programming languages relate to state machine (considering that we have focused on developing action-based languages because they are far more efficient than state-based or state-action based programming languages)
3/ the definition of a state machine that we are all familiar with (graph of states and transitions) is an approximation
4/ TLA+ introduces a new definition of state machines that is far better aligned with action-based programming languages
5/ SAM is a modest contribution that demonstrates that
Edward Mulraney
@edmulraney
Mar 21 2017 14:08
Nice, I'll check out the slides - cheers. Yeah I think that was the conclusion to our conversation in December - that the TLA+ hasn't been simply mapped to javascript in SAM, but some attempt at applying some principles from it
but I remember the definition of a TLA+ "action" wasn't 100% clear based on the text I'd found
Jean-Jacques Dubray
@jdubray
Mar 21 2017 15:17
blob
Dr Lamport defines very clearly what an action is, in his book:
Here is the book's pdf
As we spoke before, in TLA+, being a specification language, not an execution language, everything has to return a boolean value. The mathematical "execution" stops when all predicates return a false value in the next-state-predicate (i.e. the state of the system can no longer change)
In programming that approach is not practical and an alternative needs to be provided.
In SAM an action creates a proposal (primed values, i.e. the values we want the model to accept) from unprimed values, the values of the system/model in the previous state.
Jean-Jacques Dubray
@jdubray
Mar 21 2017 15:25
If you have a better interpretation, I'll take it. In any case, it does seem that Dr. Lamport's definition lands naturally as "an action is a data structure"
Jean-Jacques Dubray
@jdubray
Mar 21 2017 18:51
There is also this on HN: "Paxos in 25 lines" much clearer (just joking).