Live data from Hacker News

How core.async and CSP help you prove your async code works

reaktor.com

1–10 of 18 posts

Re: How core.async and CSP help you prove your async code works

#2
This is a bad title. The only point at which the post even talks about FRP is in the sentence "And are there practical reasons that a library based on the CSP language is useful in ways that, say, an FRP or functional reactive programming library is not?". Doesn't mention FRP after that, not even in part II.

Re: How core.async and CSP help you prove your async code works

#4
Big hairy core.async go blocks like shown in these articles makes me a tad uneasy (see the sync source in the second part to this article). Because they seem to be programmed in a mostly imperative style. Almost every time I see a go block loop, I see code that could be better written with core.async/pipeline. `If` statements can be come filters, transformations can become map. And with the addition of transducers all this becomes much cleaner.

So in that sense, I think many FRP-esque libraries have something going for them, they force their users into a model that is more declarative than imperative. That sort of programming can and should be done with core.async. Go blocks are a primitive, build abstractions on top of that and keep your app code declarative.

Re: How core.async and CSP help you prove your async code works

#5
post #2

This is a bad title. The only point at which the post even talks about FRP is in the sentence "And are there practical reasons that a library based on the CSP language is useful in ways that, say, an FRP or functional reactive programming library is not?". Doesn't mention FRP after that, not even in part II.

My bad, I just noticed that too and changed the title to reflect it. Thanks for pointing it out!

Re: How core.async and CSP help you prove your async code works

#7
> How can I know that my sync algorithm works?

TLA+ is one such language that can help you. It models computation at a higher level using the Temporal Logic of Actions. Essentially you define some variables to model your problem in and declare a bunch of next-state relations. You can then check your design against your correctness and liveness invariants to see if your expectations hold against all possible executions.

If you are so inclined you can even go as far as proving it correct.

I recently just grasped the proof of the strong-fairness property and it's amazing to me that we don't use predicate and temporal logic more frequently in software development.

There are other languages of course such as Event-B and Z, but I find for learning these concepts TLA+ is a great introduction.

[0] https://www.youtube.com/watch?v=iCRqE59VXT0

Re: How core.async and CSP help you prove your async code works

#8
The only things that have been shown are that an overly simplified CSP model of what the author is actually doing might work, that the author does not have a clear understanding of concurrency, and that the author is prone to making grandiose claims like "The matching of models means that CSP can be used to solve complex problems using core.async in a way that would be more difficult using another approach like functional reactive programming or actors", without basis.

In this particular case, uniquely-identified, timestamped property updates, with last-update-wins, for named objects, would have trivially worked, in any language, without the modelling complications. Actors, FRP and CSP are all capable of doing that, without error.

Re: How core.async and CSP help you prove your async code works

#9

The only things that have been shown are that an overly simplified CSP model of what the author is actually doing might work, that the author does not have a clear understanding of concurrency, and that the author is prone to making grandiose claims like "The matching of models means that CSP can be used to solve complex problems using core.async in a way that would be more difficult using another approach like funct…

Agreed, I'm not even convinced you need anything async here. In that sense you could probably write this with OS threads and you language of choice.

Re: How core.async and CSP help you prove your async code works

#10
post #4

Big hairy core.async go blocks like shown in these articles makes me a tad uneasy (see the sync source in the second part to this article). Because they seem to be programmed in a mostly imperative style. Almost every time I see a go block loop, I see code that could be better written with core.async/pipeline. `If` statements can be come filters, transformations can become map. And with the addition of transducers al…

The go blocks in here are really ugly, but to be honest I just found it difficult to refactor in this particular case. The issues were a) I wanted all the events in a single event loop to make timing issues clear and to fit the model semantics better b) core.async go blocks, because they are macros, can't be refactored like functions (>! and such need to be in a go block) and c) the sync logic otherwise was easier to reason about with all of the logic in one place. One better way to factor this would be to have a declarative format for what each action performs, but it ended up being more difficult to follow the logic when I refactored it this way. Types would help, and I think in general there is unexploited potential for types and CSP and FRP approaches. But if you have suggestions for how to make this better I'm all ears.
Post reply on HN