Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Keeping CALM: when distributed consistency is easy

blog.acolyer.org

Post reply on HN
Print view View original

21–30 of 48 posts

Re: Keeping CALM: when distributed consistency is easy

#21

Post by jerf »

zzzcpan wrote: post #20
jerf wrote: post #13

I expect that the continuing popularity and necessity of distributed programming is going to finally put an end to the idea that "programming doesn't involve mathematics". It is just so much easier if you approach it from the sort of mathematical mindset demonstrated in this paper, and exactly as discussed, this is going to be a whole-stack affair, not something that can be isolated to just the data layer, despite ou…

I disagree, I think the future still holds separate data layer, but even less math because of how much easier it will be to reason about programs with DSLs built on solid foundations for distributed systems and how much harder it will be to keep doing things the old ways. Imagine a new language for databases, like SQL, but that can actually guarantee convergence and coordination freedom, where there are no transactio…

I think you'll find that if you encode these guarantees into the language level itself, that won't allow the programmers involved to stop thinking about the math. Either your language won't allow them to express the first thing they want to express, and they'll have to figure out how to do it with the proper mathematical primitives (and they'll complain up a storm about how useless your language is on the forums), or it will allow them to express it but yield a compile-time "Operation violates monotonicity constraints at line 88..." and they're going to have to understand that fairly deeply, or also end up dropping your language when they can't scale up their program because the "blunder around adding and removing sigils and annotations and sprinkling in 'unsafe' until the compiler shuts up" just doesn't scale very far beyond "complete the school assignment due tomorrow".

Look at Rust. Putting memory management concerns in the language front and center doesn't relieve you from having to thinking about them. It means you have to think even more deeply about them. Fortunately, this is the correct thing to do, and it get easier with practice, and is also easier to learn when it's so strongly highlighted instead of implied and buried. But if anything, it forces a more mathematical way of thinking on to you. (Reasoning about scopes is the foundation of the mathematical discipline of structured programming.)

Re: Keeping CALM: when distributed consistency is easy

#22

Post by agentultra »

deegles wrote: post #17
agentultra wrote: post #16

Earlier quoted context omitted.

I think this has been the case for many decades. Lamport, the Turing award winning mathematician and computer scientist who wrote seminal algorithms and papers on distributed consensus, invented TLA+ for this express purpose. A programming language is insufficiently expressive enough to specify and guarantee the safety and liveness properties of a multi-agent system. I think formal methods and program synthesis are g…

What's a good small project + stack for someone to start with formal methods and/or program synthesis?

For an introduction and motivation to TLA+ I recommend Hillel Wayne's talk Everything About Distributed Systems is Terrible [0] and basically anything he has written on his blog about the TLA+.

I think following along with the TLA+ video course is really thorough and digestible once you've decided that you want to learn more [1].

You'll find the TLA+ Hyperbook is a useful reference and guide as you start specifying your own systems [2]. It has a number of examples and projects to work on.

Eventually if you want to go deep after you've decided it's worth it for yourself, get into Specifying Systems the text book and bible of TLA+ [3].

Program Synthesis has a lot of research in it and is starting to show promising results. I'd say that while the research has been going on for a long time it's still rather new to industrial use... for a motivating talk and explanation on what program synthesis is try this one: https://www.youtube.com/watch?v=HnOix9TFy1A

[0] https://www.hillelwayne.com/talks/distributed-systems-tlaplu...

[1] https://lamport.azurewebsites.net/video/videos.html

[2] https://lamport.azurewebsites.net/tla/hyperbook.html

[3] https://lamport.azurewebsites.net/tla/book.html

Re: Keeping CALM: when distributed consistency is easy

#23

Post by deegles »

agentultra wrote: post #22
deegles wrote: post #17

Earlier quoted context omitted.

What's a good small project + stack for someone to start with formal methods and/or program synthesis?

For an introduction and motivation to TLA+ I recommend Hillel Wayne's talk Everything About Distributed Systems is Terrible [0] and basically anything he has written on his blog about the TLA+. I think following along with the TLA+ video course is really thorough and digestible once you've decided that you want to learn more [1]. You'll find the TLA+ Hyperbook is a useful reference and guide as you start specifying y…

Thanks!

Re: Keeping CALM: when distributed consistency is easy

#24

Post by marcosdumay »

elierotenberg wrote: post #12

It seems like monotonicity (or a subset, stronger monotinicity, still covering many practical use cases) can be statically enforced in an algrebraic type system. With some generics magic you can encode monotonicity as a type assertion on (optionally asynchronous) function calls mapping an underlying transport/RPC mechanism (REST over HTTP, RPC over Websocket, custom protocol over TCP/domain socket...). In TypeScript…

Well, since you just need to restrict the operations one can do with data, even a Java or C++ style type system is enough.

What is best done with another language (or a complex library on a very malleable language) is permitting non-monotonic operations with a clear boundary between them and some code style that makes them undesirable.

Re: Keeping CALM: when distributed consistency is easy

#25

Post by elisharobinson »

jerf wrote: post #13

I expect that the continuing popularity and necessity of distributed programming is going to finally put an end to the idea that "programming doesn't involve mathematics". It is just so much easier if you approach it from the sort of mathematical mindset demonstrated in this paper, and exactly as discussed, this is going to be a whole-stack affair, not something that can be isolated to just the data layer, despite ou…

I'm being honest here I don't quite understand all the math involved . But from my rough skimming of the text looks like we are sacrificing the flexibility to change any input or minor design changes for guaranteed correctness .. am I wrong

Re: Keeping CALM: when distributed consistency is easy

#26

Post by amalcon »

jerf wrote: post #13

I expect that the continuing popularity and necessity of distributed programming is going to finally put an end to the idea that "programming doesn't involve mathematics". It is just so much easier if you approach it from the sort of mathematical mindset demonstrated in this paper, and exactly as discussed, this is going to be a whole-stack affair, not something that can be isolated to just the data layer, despite ou…

When people say that "programming doesn't involve mathematics", I think they really mean that programming doesn't involve hard mathematics. It's obvious that computers can only calculate, and meta-calculation is mathematics. However, most people have this notion that math is hard, and many programming tasks are easy.

Then, you take a look at a distributed system. Every task is substantially harder in a distributed system. The answers are not obvious, so folks are more willing to accept that those things are math.

Re: Keeping CALM: when distributed consistency is easy

#27

Post by jerf »

elisharobinson wrote: post #25
jerf wrote: post #13

I expect that the continuing popularity and necessity of distributed programming is going to finally put an end to the idea that "programming doesn't involve mathematics". It is just so much easier if you approach it from the sort of mathematical mindset demonstrated in this paper, and exactly as discussed, this is going to be a whole-stack affair, not something that can be isolated to just the data layer, despite ou…

I'm being honest here I don't quite understand all the math involved . But from my rough skimming of the text looks like we are sacrificing the flexibility to change any input or minor design changes for guaranteed correctness .. am I wrong

It's more like "the flexibility to change any input" produces incorrect behavior, full stop.

When it comes to distributed systems, you have to be following some mathematical idea of how you're going to maintain some sort of consistency or correctness, or it just won't happen. The environment is just so much more hostile than the ones most people are used to. Most programming methodologies haven't grown up in the presence of an adversary that, for all practical purposes, is out to get you.

Another such discipline is the security domain, and we're having the same sorts of issues there, too. As a whole community, we're really just beginning to grapple with the idea of programming in an environment that has hostile, intelligent entities out to get you. There's still a contingent of people who insist it's not even an issue! Though it's shrinking fairly rapidly.

Re: Keeping CALM: when distributed consistency is easy

#28

Post by achou »

elierotenberg wrote: post #12

It seems like monotonicity (or a subset, stronger monotinicity, still covering many practical use cases) can be statically enforced in an algrebraic type system. With some generics magic you can encode monotonicity as a type assertion on (optionally asynchronous) function calls mapping an underlying transport/RPC mechanism (REST over HTTP, RPC over Websocket, custom protocol over TCP/domain socket...). In TypeScript…

Interesting idea. Can you elaborate on the TypeScript comment? How would you encode something like this in TS?

Re: Keeping CALM: when distributed consistency is easy

#29

Post by Ar-Curunir »

jerf wrote: post #21
zzzcpan wrote: post #20

Earlier quoted context omitted.

I disagree, I think the future still holds separate data layer, but even less math because of how much easier it will be to reason about programs with DSLs built on solid foundations for distributed systems and how much harder it will be to keep doing things the old ways. Imagine a new language for databases, like SQL, but that can actually guarantee convergence and coordination freedom, where there are no transactio…

I think you'll find that if you encode these guarantees into the language level itself, that won't allow the programmers involved to stop thinking about the math. Either your language won't allow them to express the first thing they want to express, and they'll have to figure out how to do it with the proper mathematical primitives (and they'll complain up a storm about how useless your language is on the forums), or…

I mostly agree, but I think any new mathematical understanding will be an implicit one. For example, in Rust, although the underlying type system is affine, almost no one explicitly reasons about programs using affine logic

Re: Keeping CALM: when distributed consistency is easy

#30

Post by mjb »

jerf wrote: post #19
deegles wrote: post #17

Earlier quoted context omitted.

What's a good small project + stack for someone to start with formal methods and/or program synthesis?

I'd actually suggest rather becoming fluent in modern Haskell. Formal methods are great in their own way but for a lot of programming tasks they overshoot the mark. For those that do not, by all means, bring them in. But right now, a practical engineer can't ignore just how klunky they are and how badly they scale up. One may gaze longingly at them, and dream fondly of the future date when they are more practical, bu…

Many formal methods have a much simpler mathematical foundation than Haskell. For example, for TLA+ the background includes mostly (basic) set theory, basic logic, and some additional bits of temporal logic.

Some methods do require a lot more math, or different math, but I'd say your statement is false for the majority of popular formal methods.

Post reply on HN