type-safety - 静态类型的语言意味着什么？

Question

我的理解是，这意味着人们可以编写一个程序来正式证明用静态类型语言编写的程序将没有某个(小)缺陷子集。

我的问题如下:

假设我们有两种图灵完备语言，A 和 B。假定 A 是“类型安全的”，而假定“B”不是。假设我有一个程序 L 来检查用 A 编写的任何程序的正确性。是什么阻止我将任何用 B 编写的程序翻译成 A，应用 L。如果 P 从 A 翻译成 B 那么为什么不是 PL a任何用 B 编写的程序的有效类型检查器？

我接受过代数训练，刚刚开始学习 CS，所以可能有一些明显的原因这不起作用，但我非常想知道。这整个“类型安全”的事情对我来说已经有一段时间了。

Answer 1

如 您可以将每个 B'(用 B 编写的程序)翻译成等效的 A'(如果 B' 是正确的)，那么语言 B 与语言 A 享有同样多的“类型安全”(在理论上，当然;-)——基本上这意味着 B 是这样的，你可以做完美的类型推断。但这对于动态语言来说是极其有限的——例如，考虑:

if userinput() = 'bah':
    thefun(23)
else:
    thefun('gotcha')

哪里 thefun (让我们假设)对于 int 参数是类型安全的，但对于 str 参数不是。现在 - 你如何将其翻译成语言 A首先...？