是的，有些语言旨在编写可证明正确的软件。有些甚至用于工业。Spark
Ada可能是最突出的例子。我已经与Praxis
Critical Systems
Limited的一些人进行了交谈，他们将其用于在Boings上运行的代码（用于引擎监视），这看起来非常不错。（以下是该语言的精彩摘要/说明。）此语言及其随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，有两种技术可以编写正确的软件：
- 技术1：用您喜欢的语言（例如C，C ++或Java）编写软件。采取这种语言的正式规范，并证明您的程序正确。
如果您的目标是100％正确（这在汽车/航空航天业通常是必需的），那么您将花费很少的时间进行编程，而花费更多的时间进行证明。
- 技术2：以一种稍显笨拙的语言（例如，Ada的某些子集或OCaml的调整版本）编写软件，并在编写过程中编写正确性证明。在这里编程和验证是齐头并进的。在Coq中编程甚至完全等同于它们！（请参阅库里-霍华德书信）
在这些情况下，您总是会得到正确的程序。（一定会保证错误会根植于规范中。）您可能会花更多的时间在编程上，但另一方面，您会在此过程中证明它是正确的。
请注意，这两种方法都取决于您手头有一个正式的规范（您将如何分辨正确/不正确的行为）以及该语言的形式化语义（您将如何分辨实际的行为）您的程序是）。
这是正式方法的更多示例。是否是“真实世界”，取决于您问的人:-)
- Coq定理证明：用Coq编程（技术2）
- ESC / Java（技术1，虽然声音不完整）
- Spec＃（技术1，虽然声音不完整）
- Why / Krakatoa（技术2，基于Java）
我只知道一种“证明正确的” Web应用程序语言
：UR。确保“经过编译器”的Ur程序不会：
- 遭受任何形式的代码注入攻击
- 返回无效的HTML
- 包含无效的应用程序内链接
- HTML表单与其处理程序期望的字段之间不匹配
- 包括客户端代码，这些代码对远程Web服务器提供的“ AJAX”样式的服务做出了错误的假设
- 尝试无效的SQL查询
- 与SQL数据库或浏览器与Web服务器之间的通信使用不正确的封送或封送处理
