我的理解是，这意味着人们可能会编写一个程序来正式证明用静态类型语言编写的程序将没有某个（小）缺陷子集。
我的问题如下：
假设我们有两种图灵完备的语言，A 和 B。假定 A 是“类型安全的”，而假定“B”不是。假设我有一个程序 L 来检查任何用 A 编写的程序的正确性。是什么阻止我将任何用 B 编写的程序翻译成 A，应用 L。如果 P 从 A 翻译到 B，那么为什么 PL 不是用 B 编写的任何程序的有效类型检查器？
我接受过代数培训，并且才刚刚开始学习 CS，因此可能有一些明显的原因表明这不起作用，但我非常想知道。这整个“类型安全”的事情对我来说已经有一段时间了。
如果您可以将每个B'（用 B 编写的程序）翻译成等效的 A'（如果 B' 是正确的），那么语言 B 与语言 A 一样享有“类型安全”（在理论上，当然;-) - 基本上这意味着 B 是这样的，你可以进行完美的类型推断。但这对于动态语言来说是极其有限的——例如，考虑：
if userinput() = 'bah':
thefun(23)
else:
thefun('gotcha')
其中thefun（假设）对于 int 参数是类型安全的，但对于 str 参数不是。现在 - 你首先如何将它翻译成语言A......？
让 A 成为您的图灵完备语言，它应该是静态类型的，让 A' 成为您在删除类型检查时从 A 获得的语言（但不是类型注释，因为它们也用于其他目的）。A 接受的程序将是 A' 接受的程序的子集。所以特别是，A' 也将是图灵完备的。
给定您的翻译器 P 从 B 到 A（反之亦然）。它应该做什么？它可以做以下两件事之一：
首先，它可以将 B 的每个程序 y 转换为 A 的程序。在这种情况下，LPy 将始终返回 True，因为 A 的程序根据定义是正确类型的。
其次，P 可以将 B 的每个程序 y 转换为 A' 的程序。在这种情况下，如果 Py 恰好是 A 的程序，则 LPy 将返回 True，否则返回 False。
由于第一种情况没有产生任何有趣的东西，让我们坚持第二种情况，这可能就是您的意思。在 B 的程序上定义的函数 LP 是否告诉我们关于 B 的程序的任何有趣的事情？我说不，因为它在 P 的变化下不是不变的。由于 A 是图灵完备的，即使在第二种情况下，也可以选择 P 使其图像恰好位于 A 中。那么 LP 将始终为真。另一方面，可以选择 P，以便将一些程序映射到 A' 中的 A 的补码。在这种情况下，LP 会为 B 的一些（可能所有）程序吐出 False。正如你所看到的，你没有得到任何只取决于 y 的东西。
我也可以用以下方式更数学地说：有一类 C 编程语言，其对象是编程语言，其态射是从一种编程语言到另一种编程语言的翻译器。特别是如果存在态射 P: X -> Y，则 Y 至少与 X 一样具有表达能力。在每对图灵完备语言之间，存在两个方向的态射。对于 C 的每个对象 X（即，对于每种编程语言），我们都有一个关联的集合，比如说 {X}（我知道这是不好的表示法）可以由 X 的程序计算的那些部分定义的函数。每个态射 P：X - > Y 然后引发集合 {X} -> {Y} 的包含。让我们正式反转所有导致恒等式 {X} -> {Y} 的态射 P: X -> Y。我将调用结果类别（用数学术语来说，由 C' 对 C) 的本地化。现在包含 A -> A' 是 C' 中的态射。然而，它在 A' 的自同构下不被保留，即态射 A -> A' 不是 C' 中 A' 的不变量。换句话说：从这个抽象的角度来看，“静态类型”属性是不可定义的，可以任意附加到语言上。
为了更清楚地说明我的观点，您还可以将 C' 视为 3D 空间中的几何形状的类别，并将欧几里得运动视为态射。A' 和 B 是两个几何形状，P 和 Q 是将 B 带到 A' 的欧几里得运动，反之亦然。例如，A' 和 B 可以是两个球体。现在让我们在 A' 上固定一个点，它代表 A' 的子集 A。让我们称这一点为“静态类型”。我们想知道 B 的一个点是否是静态类型的。所以我们取这样一个点 y，通过 P 映射到 A' 并测试它是否是我们在 A' 上的标记点。很容易看出，这取决于选择的映射 P，或者换句话说：球体上的标记点不会被该球体的自同构（将球体映射到自身上的欧几里得运动）保留。
没有什么“可疑”的。;)
相对于任何非平凡 [ 1 ] 类型系统T是类型安全的图灵完备语言集是图灵完备语言的严格子集。因此，在一般情况下，不存在从B到A 的翻译器P -1；因此，任何翻译器兼类型检查器LP -1也没有。
对这种说法的下意识反应可能是：胡说八道！A和B都是图灵完备的，所以我可以用任何一种语言表达任何可计算的函数！而且，确实，这是正确的——你可以用任何一种语言表达任何可计算的函数；然而，很多时候，你也可以表达更多。特别是，您可以构造指称语义没有明确定义的表达式，例如那些可能很乐意尝试对字符串“foo”和“bar”进行算术和的表达式（这是丘布斯达 亚历克斯·马泰利的回答）。这些类型的表达式可能在语言B中“使用”，但在语言A中可能根本无法表达，因为指称语义未定义，因此没有明智的翻译方式。
这是静态类型的一大优势：如果您的类型系统在编译时无法证明上述函数将接收除算术加法运算符的结果已明确定义的参数之外的任何参数，它可以被拒绝为错误类型。
请注意，虽然以上是解释静态类型系统优点的常用示例，但它可能过于谦虚。一般而言，静态类型系统不必仅限于强制参数的类型正确性，而是确实可以表达程序的任何期望属性，这些属性可以在编译时证明。例如，可以构建类型系统来强制释放文件系统句柄（例如，对数据库、文件、网络套接字等）在获取文件系统句柄的同一范围内的约束。显然，这在生命支持系统等领域非常有价值，在可证明的情况下尽可能多的系统参数的正确性是绝对必要的。如果你满足静态类型系统，你可以免费获得这些证明。
[ 1 ] 我的意思是，并非所有可能的表达式都是类型良好的。
提出与已提出的相同观点的另一种方法是，您的问题构成了矛盾的证明，即：
或两者。我的直觉说后者可能是症结所在：类型安全是一种元语言属性。
我的理解是，这与编译时与运行时有关。在静态类型语言中，大多数类型检查是在编译时执行的。在动态类型语言中，其大部分类型检查是在运行时执行的。
让我反过来回答这个问题：
有两种不同类型的“动态”编程。
一个是“动态类型”，这意味着您有某种外壳，您可以通过在该外壳中键入定义来进行编程，就像 Python 的空闲外壳一样。
另一种类型的动态规划，是一种更具理论性的规划。动态程序是可以更改其自身源的程序。它需要某种程度的注入，并且通常用于更改微控制器上的程序存储器。有时为数字运算生成查找表称为动态规划。