Jangda等人由于在“无服务器计算的形式基础”方面的工作而在今年获得了OOPSLA的杰出论文奖。本文的中心是他们观察到无服务器执行环境具有许多独特的属性（例如执行环境的热启动/重用），这会使构建正确的应用程序变得更加困难。它们显示了无服务器功能可以安全地忽略这些特性的条件，因此变得更容易推论。他们还介绍了一种基于箭头的合成语言，用于函数合成。
无服务器时要注意的事项：
尽管无服务器计算抽象有很多优点，但它暴露了一些低级别的操作细节，使程序员难以编写代码和推理代码。例如，为了减少延迟，无服务器平台尝试重用同一功能实例来处理多个请求。但是，此行为不是透明的，很容易编写无服务器函数，该函数在重新使用时会产生错误的结果或泄露机密数据。一个相关的问题是无服务器平台在空闲时突然终止函数实例…
这个问题与无服务器环境中的误用/误解状态有关。无服务器功能是无状态的，但是可以在调用之间适当地重用缓存的状态以加快启动时间。
“做错事”的示例有一个代码样本：
let accounts = new Map(); // account_name -> balance |
如果您试图将“持久”状态保持在无法正常运行的无服务器函数中！不要那样做！更有可能陷入困境的是缓存某些状态以在函数执行之间进行机会性重用，但是这种状态只能与指定用户相关联，根本无法保证下一次执行针对的还是同一用户。
第二个考虑因素是函数的许多实例可以并行执行（这不是重点吗？！）。没有函数相似性的概念，因此来自同一源的请求也可能由不同的函数实例处理。因此，您可能需要一种在函数执行环境之外的共享状态的协调机制（例如，具有事务支持的持久性存储）。
第三个考虑因素肯定会更加棘手。考虑到至少执行一次的语义（即事件可以重试，具体取决于您配置重试策略的方式），它涉及对等幂性的需求。
大多数平台响应单个事件至少运行一次函数，当函数产生副作用时，这可能会导致问题。
如果您的函数不是自然幂等的，则可能需要采取一些策略，例如记住以前看到的事件ID。作者在这里没有提到的是，只有当非幂等性涉及事务资源管理器所执行的操作（您还用于存储已处理的事件ID）并且正在使用事务时，这才真正起作用。如果函数是发送电子邮件，那么副作用很显然无法收回这些邮件，祝您好运！
更多有关数学形式推理可点击标题见原文