These are chat archives for jdubray/sam

15th
Mar 2018
Jean-Jacques Dubray
@jdubray
Mar 15 2018 01:58
Paolo Furini
@pfurini
Mar 15 2018 09:56
What do you think? https://www.idris-lang.org/ and the first chapter of a Mapt book I was reading this morning: https://livebook.manning.com/#!/book/type-driven-development-with-idris/chapter-1
Bear in mind that I'm not talking of possible "production" uses of Idris, but I found it really interesting from an academic point of view (especially the "type-driven" approach)
Riccardo Ferretti
@riccardoferrett_twitter
Mar 15 2018 10:18
for experiments, MVPs and POCs that's nearly always true.. but in other cases I plan ahead and define the constraints of the final product. For example I'll need plenty of storage, and that's pretty much expensive with Firebase (and google cloud in general), but I already found an hybrid approach to leverage both a firebase storage and an external storage at a lower cost
@pfurini what approach have you found? ^^
@jdubray have you come across this? https://www.hillelwayne.com/post/tla-redux/
Riccardo Ferretti
@riccardoferrett_twitter
Mar 15 2018 10:33
I am struggling to wrap my head around it..
(I am also not familiar with PlusCal, which isn't quite the most friendly language)
my understanding: this is modelling Redux behavior in TLA+/PlusCal, so the spec is Redux, not TLA+. That's why the model is implemented in that way (which is different from what a SAM-like implementation would look like, as there is no separation between action and control state).
So basically the syntax is TLA+, but the semantics are redux
Riccardo Ferretti
@riccardoferrett_twitter
Mar 15 2018 10:40
also, the constraints about the "Safe Global State" modification of the model outside of the reducer is due to the fact that the action has "direct" access to the model, which would be a non-issue in a SAM-like implementation with an "accept" step
that's my gut feeling, but I am not really sure and don't think I fully grasp the model, was curious to hear your take
(possibly even see what a SAM-like implementation would look like)