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

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

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

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

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

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

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

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

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


c cross-platform programming-languages high-level
person K.Steff    schedule 20.03.2012    source источник
comment
Вы смотрели на С++? Это (может быть) системный язык высокого уровня.   -  person Seth Carnegie    schedule 20.03.2012
comment
Да, но сложность, привносимая C++, мне кажется, не стоит дополнительных усилий. Кроме того, каждый компилятор на этой земле поддерживает другую часть языковых стандартов и, например, исключения, это беспорядок. То же самое касается RTTI и вообще каждой функции, которая делает C++ более высоким уровнем.   -  person K.Steff    schedule 20.03.2012
comment
Если вам действительно просто не нравится C++, вы можете взглянуть на D, который помимо прочего имеет сборщик мусора и менее сложен, чем C++. Хотя он намного менее популярен и не имеет столько библиотек, но может взаимодействовать с кодом C, как C++. Однако ни один из этих языков на самом деле не компилируется в C, они компилируются в машинный код.   -  person Seth Carnegie    schedule 20.03.2012
comment
Да, вы, вероятно, правы насчет C++ и D. Честно говоря, я напуган C++. Может быть, это слишком много. Эффективный С++, который я читал :) Проблема истинной кроссплатформенности остается для D, а С++ на самом деле не очень хороший язык для формальной проверки и/или формальных спецификаций.   -  person K.Steff    schedule 20.03.2012
comment
Ни один язык не подходит более или менее для формальных спецификаций, просто напишите свой код, чтобы делать то, что говорят спецификации, независимо от того, какой язык вы используете. И вы говорите, что вам нужна формальная проверка, но недетерминизм не является проблемой? Опять же, я не думаю, что какой-либо язык более или менее подходит для этого, пока вы не перейдете к таким языкам, как Haskell. Я не думаю, что что-то в точности похожее на то, что вы хотите, доступно в настоящее время. Я думаю, это зависит от инвестиций, которые вы можете сделать, чтобы выучить язык. И да, я понятия не имею о кроссплатформенности с D, я особо им не пользовался, просто читал об этом.   -  person Seth Carnegie    schedule 20.03.2012
comment
Вы делаете правильное замечание о недетерминизме, я укажу, что я имею в виду недетерминизм с точки зрения времени. Насчет "формальной верификации" не соглашусь - для C есть инструменты, а для C++ верификация значительно сложнее. Как вы указали, Haskell и многие чисто функциональные языки отлично справятся с этой задачей.   -  person K.Steff    schedule 20.03.2012
comment
Ладно, надеюсь, ты найдешь то, что ищешь.   -  person Seth Carnegie    schedule 20.03.2012
comment
возможный дубликат Какие языки/реализации общего назначения компилируются в C< /а>   -  person n. 1.8e9-where's-my-share m.    schedule 20.03.2012
comment
Я не могу читать по-английски, так как я только учу его менее чем за месяц. Но, может быть, вы можете попытаться скомпилировать схему или другой код, похожий на lisp, в c. Есть много компиляторов, которые могут это сделать.   -  person madper    schedule 20.03.2012
comment
Сет, я слышал, что формально проверить код C++ нетривиально, и это объясняет мне, почему OP ищет языки, разработанные с учетом проверки.   -  person Artyom Shalkhakov    schedule 20.03.2012
comment
Компилятор Glasgow Haskell IIRC имеет серверную часть C.   -  person Alexandre C.    schedule 20.03.2012

Ответы (2)


arrow_upward
3
arrow_downward

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

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

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

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

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

person Artyom Shalkhakov    schedule 20.03.2012
comment
+1, это самый близкий ответ на то, что мне нужно, однако на первый взгляд кажется, что сгенерированный код C требуется компилировать только с помощью GCC, который, хотя и работает на многих платформах, не доступен повсеместно. - person K.Steff; 20.03.2012
comment
@K.Steff, если вам действительно нужен язык, который компилируется в C, который может быть скомпилирован любым компилятором C, то это проблема. Тем не менее, я думаю, вы могли бы остановиться на некоторых конкретных компиляторах (скажем, GCC и Clang), которые удовлетворяли бы ваши потребности на данном этапе. Затем мы могли бы работать вместе, чтобы сделать ATS компилируемым с помощью Clang (я помню, что файлы C делали компилируемые с помощью Clang в прошлый раз, когда я пытался, но некоторые заголовки отсутствовали, так что...). Если вам нужна какая-то экзотическая платформа/компилятор, пожалуйста, будьте более конкретными; может и у нас получится. - person Artyom Shalkhakov; 21.03.2012

arrow_upward
2
arrow_downward

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

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

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

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

person jfs    schedule 20.03.2012
comment
Спасибо, что-то полезное, поищу :) - person K.Steff; 20.03.2012