TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?

I've heard Alloy is easier to learn. That being said, Alloy and TLA+ are both languages for specifications, so they can't prove an implementation is correct.

Nobody mentioned Agda. I had to use Alloy in the university and it was easy, but it doesn't cover all bases as the previous commenter said.

I found this short paper really interesting to understand the fundamental limitations of distributed systems: Consistency Tradeoffs in Modern Distributed Database System Design http://www.cs.umd.edu/~abadi/papers/abadi-pacelc.pdf . The theorem introduced in the paper (PACELC) provides a better way to understand the design of modern distributed systems than CAP.

This paper was published in PaPoC 2020, which was recently organized online. The rest of the papers, along with the talks are available here: https://papoc-workshop.github.io/2020/programme.html

The rest of the material from the summer school is available here: https://sptdc.ru/schedule/

There's also an extension which overlay the alt tags over images: https://github.com/ageitgey/show-facebook-computer-vision-ta...

>Is there a proper book(s)/source(s) that I should follow?

You may find these book useful:

Competitive Programming 3 by Felix Halim and Steven Halim.

Competitive Programmer’s Handbook (https://cses.fi/book/index.html)

>I have rarely found the need to code one up in my job

Depending on your job profile, these data structures may not be used at all. But programming puzzles have become the norm for interviews in the industry.

I have been using Zim[0] for quite few years now. With various plugins, it allows me to write LaTeX equations, formatted code, tables etc. Overall it has been really good, but I feel the only thing missing is the support for mobile devices.

[0]: http://zim-wiki.org/

This notepad app does support LaTeX equations (instructions are in the help notepad). Sadly it might be an issue on mobile for you too.

MicroPad _works_ on mobile, but not very nicely. That is a key thing I want to improve though.

The former paper appeared in SIBVOIK 2017 (http://www.sigbovik.org/), where you can find other such papers. My personal favorites are "On The Turing Completeness of PowerPoint" (https://www.youtube.com/watch?v=uNjxe8ShM-8) and "Automated Distributed Execution of LLVM code using SQL JIT Compilation"

> Following the popularity of MapReduce, a whole ecosystem of Apache Incubator Projects has emerged that all solve the same problem. Famous examples include Apache Hadoop, Apache Spark, Apache Pikachu, Apache Pig, German Spark and Apache Hive [1]

Slightly OT, but I wanted to know if there's any group/forum where we can read and discuss papers regularly?

I know the morning paper (https://blog.acolyer.org/), but it is not so interactive, in the sense that you can't have discussions with peers and it turns into just passive reading.

If you're in Boston, we have a reading group for machine learning papers. We'll start up again on the 9th.

List of papers we've discussed: https://github.com/pmiller10/cambridge-ai

Mailing list: http://mailman.mit.edu/mailman/listinfo/sipb-deeplearning

At Spotify, we have a reading group. I started one at SoundCloud and at Google there were multiple focused on very specific topics. If you can prove to your company the value in investing in a reading group, you can probably start one in your company too.

KTH, Stockholm's main technical university, has an open reading group too, open to everyone. Probably if you have a big enough university in your area they have something similar.

Alternatively try reddit, ie.: on r/machinelearning. That said, the value of doing this in real life, in front of a whiteboard, is worth going extra mile and find someone to team up with.

Not exactly what you're looking for, but maybe you or someone else might be interested on this: http://fermatslibrary.com

Very interesting, thanks!

Somewhat related,a general purpose annotation platform is http://hypothes.is - a great feature is that PDF annotations are location independent because they use some kind of fingerprint to identify the document.

Yeah, I'd be interested in this too. Something with a lot of discussion, smallish group, to create a sense of social obligation...

(So easy to be lazy w/ the infinite world of distractions available.)

Obligatory XKCD for operating systems: https://xkcd.com/1508/