如果可能的话，我正在寻找一种更高级的系统语言，它适用于形式验证，可以编译为标准 C，以便它可以以（相对）低开销跨平台运行。
在过去的几天里，我偶然发现的两种最有前途的此类语言是：
BitC - 虽然这种语言的设计目标符合我的需求（它甚至支持功能范式），但它处于非常不稳定的状态，文档已经过时，而且，一般来说，这似乎是一个非常遥远的现实——世界项目。
Lisaac - 它支持按合同设计，非常酷并且性能开销相对较低。但是该网站已经死了，自 08 年以来就没有新版本了，而且通常看起来语言已经死了。
我还想指出，它不适用于实时系统，因此 GC 或通常的非确定性（在实时意义上）不是问题。
该项目主要涉及音频处理，但它必须是跨平台的。
我想有人会指出我明显的答案——“普通的 C”。虽然它确实是跨平台的并且非常有效，但代码量可能会更大。
编辑：我应该澄清我的意思是跨平台和跨架构。这就是为什么我只考虑语言，首先编译为 C，但如果你能指出另一个例子，我将不胜感激:)
我想你可能会对ATS感兴趣。它编译为 C （实际上它从形式类型理论的角度表达和解释了许多 C 习语和模式，甚至有人提议准备一本书来展示这一点——如果我们有更多的时间......）。
该项目主要涉及音频处理，但它必须是跨平台的。
我对音频处理了解不多，我主要是在做一些计算机图形的东西（主要是基本的东西，只是为了尝试一下）。
另外，我不确定 ATS 是否适用于 Windows（从未尝试过）。
（免责声明：我使用 ATS 已经有一段时间了。它是庞大而庞大的语言，有时难以使用，但我非常喜欢我能够用它制作的程序的质量，例如，请参阅一些实际程序的GLES2 绑定中的TEST 子目录）
以下内容并不严格遵守要求，但我还是想提一下，评论太长了：
Pypy 的 RPython 可以翻译成 C 语言。这里好好谈谈。它已被用于实现Smalltalk、JavaScript、Io、Scheme、Gameboy（具有不同程度的完整性），但您可以在其中编写独立程序。它主要以其在 Intel x86 (IA-32) 和 x86_64 平台上运行的 Python 语言的实现而闻名。
翻译过程需要有能力的 C 编译器。工具链提供了推断关于代码（由翻译过程本身使用）的各种信息的方法，您可以将其重新用于形式验证。
如果您同时了解 Python 和 C，则可以使用 cython 将类似 Python 的语法转换为 C。它用于编写 CPython 扩展。