冷水澡：当人们对一些事情过于兴奋时

当人们对一些事情感到兴奋时，这是很棒的，但有时他们会有点太兴奋了。这是一份令人敬畏的(严格和尊重的)和精心策划的(我阅读每一个建议并做出判断)关于过度炒作的话题的冷水浴清单。这并不意味着热情是坏的或错的：我们只是提醒人们要脚踏实地。您可以随时提交您最喜欢的作品！

炒作：正式验证是编写软件的好方法。我们应该证明我们所有的代码都是正确的。

Showing：广泛的文献回顾表明，正式的方法很难学习，应用起来非常昂贵，而且经常会漏掉关键的错误。

注意事项：编写于2000年，不包括现代工具/技术，如TLA+或依赖类型。

注：彼得·古特曼论文的一部分，“密码安全体系结构的设计和验证”。

Showing：对所有可用文献(截至2014年)的回顾表明，坚实的研究不是决定性的，而结论性的研究存在方法论问题。

注意事项：不包括静态类型的其他可能好处，如文档。不涉及渐进式字体系统的研究，如mypy或tyescript。

Showing：将在128核群集上运行的尖端图形处理算法与单线程2014 Macbook Pro进行基准比较。笔记本电脑总是胜出，有时会领先一个数量级。

警告：McSherry非常擅长优化他的算法，并且拥有一般数据科学家所没有的技能。如果您有即席查询，并且不想花时间对其进行优化，那么大数据系统可能会更好。

注意：如果你打算自己使用大数据系统，看看它是否比你的笔记本电脑快。如果你要为别人建立一个大数据系统，一定要确保它比我的笔记本电脑还快。"；

注意事项：原始数据你必须自己解读。不会为您自己的分析提供原始数据的完整转储。现在可以在此处找到原始数据。

注：不断更新新的基准。所有的实现都是公开的，您可以通过公关来改进它们。

Showing：回顾敏捷的所有不同风格，以及一些实践(特别是用用户故事替换需求和缺乏适当的规范)在长期内是如何有害的。

警告：虽然Meyer指出了一些问题，但总的来说，他对敏捷非常积极，并推荐它作为一种好的(但不完美的)方法。

淋浴：研究人员查看了三个经过正式验证的系统，发现这三个系统都存在严重的正确性错误。这些错误来自一系列不匹配的假设，并导致服务器崩溃或产生错误数据。

警告：大多数错误都在系统边界；在实现的协议中没有发现任何错误。正式验证的系统虽然不完美，但比未经验证的系统缺陷要少得多。

Showing：研究人员让程序员修复代码库中的错误，要么所有标识符都缩写，要么所有标识符都是完整的单词。他们发现调试所用的时间和质量没有差别。

警告：仅适用于修复错误。否则就无懈可击了。老实说，这是我读过的最严谨、最全面的论文之一。

注意：包括关于程序员如何调试缩写代码的人种学。链接指向作者的预印本。

淋浴：提出了五种谬论，说明为什么微服务解决了巨型计算机所存在的问题，并说明了微型计算机实际上并不存在这些问题，或者微服务使问题变得更糟。

炒作：你最喜欢的编程语言已经更新了。新版本提出了令人印象深刻的性能改进主张。

阵雨：在近乎理想的环境下对现代编程语言进行基准测试，只是时间比以前长，这表明我们没有像我们希望的那样准确地对语言实现进行基准测试。随着时间的推移，许多基准测试都会变慢。有些人永远不会稳定下来。由于不确定性，许多基准实验将无法重复。热身时间很重要，但通常要么被忽视，要么被不准确地报道。

注意事项：仅评估x86_64架构，且仅针对两个操作系统(Linux和OpenBSD)。在2017年进行的实验(在进行深入修补之前)。主要评估JITted语言实现(尽管包括C基准)。

注：实验和Benchmark Runner是在开源许可下发布的。从这里开始。

炒作：横向扩展比纵向扩展要好。云比裸机更具扩展性。

Showing：Expensify发现运行单个裸机服务器比使用x1e.32xLarge EC2实例更快、更便宜。通过使用一台服务器，他们可以避免对数据进行分片。

警告：不包括横向扩展裸机是否与横向扩展EC2具有相同的优势(假设您负担得起切分)。无法真正比较裸机有多便宜，因为他们没有列出成本。我猜他们的服务器各有10万台吧？不过，这种猜测是没有根据的。