LangInteger

This is a note reading the thesis of Lionel Blatter¹, which makes contribution to the relational properties verification in the Frama-C ecosystem, and it is also a good material for learning formal verification.

This blog compares proving type soundness using traditional progress/preservation methods and logical relations¹. Credits go to the original author of these ideas.

This is my note learning Linear Logic by Frank Pfenning.

This is a note for my learning of Constructive Logic by Frank Pfenning. Logic is the study of the principles of valid inferences and demonstration, which constitutes an important area in the disciplines of philosophy and mathematics.

In the past first semester of my Ph.D. in computer science, my attention was attracted by the study of Alonzo Church and Alan Turing, specifically, the Turing Machine developed by Alan Turing in 1936, and the lambda calculus developed by Alonzo Church in 1930, which turns out to be Turing complete and is equivalent in omputational power with Turing Machine.

TL;DR

• Zookeeper always avoids Split Brain problem with it’s majority rule for quorum
• When network partition happens, the group with the majority of nodes (if it exists) can continue to serve read and write requests
• When network partition happens, the group with minority nodes can not continue to serve write requests but can continue to serve read requests with client and server properly configured. It is obvious that read requests in this case will return stale values.

Push notification is a killer feature for engaging users and keeping them informed. In recent development of a mobile app, we integrate APNS(Apple Push Notification service) and FCM(Firebase Cloud Messaging) to our iOS/Android app based on Untiy after overcoming several obstacles which I want to share with you here.

Nowadays, Redis is an indispensable middleware in building the backend service of an app. As an ambitious team, we bought a Redis cluster under Amazon ElastiCache with the following features:

• Clustered with several shards, and each shard owns 3 nodes (each shard performs primary-replica)
• Encryption in transit enabled (or TLS) to assure no man-in-the-middle attack
• Redis AUTH enabled (of course we do not want a door without a key)

So far so good, it seems that we can concentrate on developing our product now. But wait, as the title says, the way is too long to get there!