编译成c语言的高级系统语言？

Question

我正在寻找一种更高级的系统语言，如果可能的话，适合于正式的验证，它可以编译成标准C，这样它就可以以(相对)低的开销跨平台运行。

在过去几天里，我遇到的两种最有前途的语言是：

1. BitC --尽管这种语言的设计目标符合我的需求(它甚至支持功能范例)，但它处于非常不稳定的状态，文档已经过时，一般来说，对于一个现实世界的项目来说，这似乎是一个很长的时间。
2. Lisaac -它支持按合同设计，这是非常酷和有一个相对较低的性能开销.然而，该网站已经死了，自08年以来就没有发布过新版本，一般来说，该语言似乎已经死了。

我还想指出的是，它并不适用于实时系统，因此GC或者一般的非确定性(在实时意义上)并不是一个问题。

该项目主要涉及音频处理，尽管它必须跨平台。

我想有人会给我指一个显而易见的答案--“普通的C”。虽然它是真正的跨平台和非常有效的，代码数量可能会更大。

编辑:我应该澄清一下，我指的是跨平台和跨架构。这就是为什么我只考虑将语言编译成C语言的原因，但如果您能指出另一个例子，我将不胜感激:)

Answer 1

我想你可能会对苯丙胺类兴奋剂感兴趣。它编译成C(实际上，它从形式类型理论的角度来表达和解释许多C成语和模式，甚至有人提议编写一本书来说明这一点--如果我们有更多的时间.)。

该项目主要涉及音频处理，尽管它必须跨平台。

我对音频处理不太了解，我一直在做一些计算机图形学方面的工作(主要是一些基本的东西，只是为了尝试一下)。

此外，我也不确定ATS是否在Windows上工作(从未尝试过)。

(免责声明:我已经和ATS合作了一段时间了。它是一种庞大的语言，有时很难使用，但我非常喜欢用它制作的程序的质量，例如，一些实际的程序见GLES2绑定中的TEST子目录)

Answer 2

以下内容并不严格遵守这些要求，但我还是想提一提，它太长了，不能发表评论：

Pypy的RPython可以翻译成C. 这里有个很好的话题。它被用来实现Smalltalk，JavaScript，Io，Scheme，Gameboy (具有不同程度的完整性)，但是您可以在其中编写独立的程序。它主要以其对64个平台语言的实现而闻名。

翻译过程需要一个有能力的C编译器。工具链提供了推断代码(翻译过程本身使用的)的各种内容的方法，您可以将其重新用于正式验证。

如果您同时了解Python和C，可以使用cython将类似Python的语法转换为C。它用于编写CPython扩展。