开放世界中的渐进类型化

渐进类型化在同一语言中结合了静态与动态类型化，为程序员提供了两者的优势。静态类型化提供错误检测和强保证，而动态类型化支持快速原型开发和灵活的编程习惯用法。然而，为了让程序员充分利用渐进类型系统，他们必须能够信任其类型注解，因此必须在静态与动态代码的边界执行运行时检查，以确保静态类型得到遵守。高阶和可变值无法在这些边界被完全检查，因此必须在其使用点执行额外检查。传统上，这是通过在此类值上安装包装器或代理来实现的，这些包装器或代理调节静态与动态之间的数据流，但如果语言支持对象标识比较或具有外部函数接口，则可能导致问题。Reticulated Python 是通过 Python 3 的源到源翻译器实现的 Python 渐进类型化变体。它实现了一种名为瞬态强制转换（transient casts）的无代理替代设计。本文为瞬态强制转换提供了形式语义，并表明它们不仅是可靠的，而且适用于开放世界环境，其中仅对部分程序应用了 Reticulated 翻译器；其余为未翻译的 Python。我们形式化了这一开放世界可靠性属性，并使用 Coq 证明它对于 Anthill Python（一种对 Reticulated Python 建模的演算）成立。