An empirical study on the correctness of formally verified distributed systems
We must recognise that even formal verification can leave gaps and hidden assumptions that need to be teased out and tested, using the full battery of testing techniques at our disposal. Building distributed systems is hard. But knowing that shouldn’t make us shy away from trying to do the right thing, instead it should make us redouble our efforts in our quest for correctness.
(tags: formal-verification software coding testing tla+ chapar fuzzing verdi bugs papers)
After Seven Years, Microsoft Is Finally Fixing the “J” Email Bug
True story: when I started at Amazon, I thought people were using “J” instead of smileys as shorthand for “joking”. Great job Microsoft! (via Tony Finch)
(tags: microsoft fail operating-systems monoculture character-sets j wingdings exchange email)
-
Pembrolizumab, marketed by Merck as Keytruda, is an anti-PD-1 immunotherapy drug now going through US trials, targeting malignancies with certain molecular characteristics. Good trial results vs melanoma here: http://www.nejm.org/doi/full/10.1056/NEJMoa1503093
(tags: cancer trials drugs pembro anti-pd-1 immunotherapy merck)
Scaling Amazon Aurora at ticketea
Ticketing is a business in which extreme traffic spikes are the norm, rather than the exception. For Ticketea, this means that our traffic can increase by a factor of 60x in a matter of seconds. This usually happens when big events (which have a fixed, pre-announced ‘sale start time’) go on sale.
(tags: scaling scalability ops aws aurora autoscaling asg)