Системный язык высокого уровня, который компилируется в c?

Question

Я ищу системный язык более высокого уровня, по возможности, подходящий для формальной проверки, который компилируется в стандарт C, чтобы его можно было запускать кроссплатформенно с (относительно) низкими издержками.

Два самых многообещающих таких языка, на которых я споткнулся за последние несколько дней:

1. BitC - хотя цели разработки этого языка соответствуют моим потребностям (он даже поддерживает функциональную парадигму), он находится в очень нестабильном состоянии, документация устарела, и, как правило, это выглядит очень долго для реального проекта.

2. Lisaac - поддерживает дизайнпо контракту, что очень круто и имеет относительно низкую производительность.Тем не менее, веб-сайт мертв, с 2008 года не было выпущено ни одной новой версии, и в целом кажется, что язык мертв.

Я также хотел бы отметить, что он не предназначен длясистема реального времени, то есть GC или, как правило, недетерминизм (в смысле реального времени), не является проблемой.

Проект включает в себя в основном обработку звука, хотя он должен быть перекрестнымплатформа.

Я предполагаю, что кто-то укажет мне на очевидный ответ - "обычный старый".Хотя он действительно кроссплатформенный и очень эффективный, количество кода, вероятно, будет больше.

РЕДАКТИРОВАТЬ: я должен уточнить, что я имею в виду кроссплатформенность и кросс-архитектуру.Вот почему я рассматриваю только языки, скомпилированные в первую очередь в C, но если вы можете указать мне другой пример, я был бы благодарен:)

Answer 1

Я думаю, вы можете заинтересоваться ATS .Он компилируется в C (на самом деле он выражает и объясняет многие идиомы и шаблоны языка C с формальной точки зрения теории типов, даже было предложено подготовить книгу своего рода, чтобы показать это - если бы у нас было больше времени ...).

Проект включает в себя, в основном, обработку звука, хотя он должен быть кроссплатформенным.

Я мало что знаю об обработке звука, я в основном занималсянекоторые элементы компьютерной графики (в основном базовые, просто чтобы попробовать).

Кроме того, я не уверен, что ATS работает в Windows (никогда не пробовал).

(Отказ от ответственности: IЯ работал с ATS в течение некоторого времени. Это громоздкий и большой язык, а иногда и сложный в использовании, но мне очень понравилось качество программ, которые я смог создать с его помощью, например, см. подкаталог TEST в привязки GLES2 для некоторых реалистичных программ)

Answer 2

Следующее строго не соответствует требованиям, но я все равно хотел бы упомянуть об этом, и это слишком долго для комментария:

RPython Pypy можно перевести на C. Вотхороший разговор об этом .Он использовался для реализации Smalltalk, JavaScript, Io, Scheme, Gameboy (с различной степенью полноты), но вы можете писать в нем автономные программы.Он известен главным образом своей реализацией языка Python, который работает на платформах Intel x86 (IA-32) и x86_64 .

Для процесса перевода требуется способный компилятор Си.Инструментарий предоставляет средства для вывода различных вещей о коде (используемом самим процессом перевода), которые вы могли бы повторно использовать для формальной проверки.

Если вы знаете и Python, и C, вы можете использовать cython, который переводит Python-подобный синтаксисна C. Используется для написания расширений CPython.