Linguaggio di sistema di alto livello che compila in c?

Question

Sto cercando un linguaggio di sistema di livello superiore, se possibile, adatto per la verifica formale, che compila lo standard C, in modo che possa essere eseguito su più piattaforme con sovraccarico (relativamente) basso.

I due più promettenti queste lingue che ho imbattuto negli ultimi giorni sono:

1. BitC - Mentre gli obiettivi di progettazione di questo linguaggio corrispondono alle mie esigenze (supporta anche il paradigma funzionale), si è in uno stato molto instabile, la documentazione non è aggiornata e, in genere, sembra una ripresa molto lunga per un progetto del mondo reale.

2. Lisaac - Supporta Design-by-contract, che è molto interessante e ha un overhead di prestazioni relativamente basso. Tuttavia, il sito Web è morto, non c'è stata una nuova versione dal 2008 e in genere sembra che la lingua sia morta.

Vorrei anche sottolineare che non è pensato per un sistema in tempo reale, in modo da un GC o, in generale, non il determinismo (nel senso in tempo reale), non è un problema.

Il progetto riguarda principalmente l'elaborazione audio, sebbene debba essere multipiattaforma.

Presumo che qualcuno mi indichi la risposta ovvia: "plain ol 'C". Sebbene sia veramente multipiattaforma e molto efficace, la quantità di codice sarebbe probabilmente maggiore.

EDIT: Vorrei chiarire che intendo cross-platform E cross-architecture. Questo è il motivo per cui considero solo le lingue, compilate per C in primo luogo, ma se riesci a indicarmi un altro esempio, ti sarei grato :)

Answer 1

Penso che potresti interessarti di ATS. Si compila a C (in realtà esprime e spiega molti idiomi e schemi C da una prospettiva teorica formale di tipo, è stato persino proposto di preparare un libro di sorta per dimostrarlo - se solo avessimo avuto più tempo ...).

Il progetto riguarda principalmente l'elaborazione audio, sebbene debba essere multipiattaforma.

Non so molto sull'elaborazione dell'audio, ho fatto principalmente alcune cose di grafica per computer (principalmente le cose di base, solo per provarlo).

Inoltre, non sono sicuro che ATS funzioni su Windows (non l'ho mai provato).

(Disclaimer: Lavoro con ATS da un po 'di tempo, linguaggio ingombrante e ampio, a volte difficile da usare, ma mi è piaciuta molto la qualità dei programmi che sono riuscito a produrre con esso, per esempio, vedere Test sottodirectory nella GLES2 bindings per alcuni programmi realistici)

Answer 2

Quanto segue non strettamente aderire ai requisiti ma mi piacerebbe parlare del fatto che in ogni caso ed è troppo lungo per un commento:

PyPy di RPython può essere tradotto in C. Here's a nice talk about it. È stato utilizzato per implementare Smalltalk, JavaScript, Io, Scheme, Gameboy (con vari gradi di completezza), ma è possibile scrivere programmi autonomi al suo interno. È noto principalmente per la sua implementazione del linguaggio Python che è runs on Intel x86 (IA-32) and x86_64 platforms.

Il processo di traduzione richiede un compilatore C capace.La toolchain fornisce i mezzi per dedurre varie cose sul codice (utilizzato dal processo di traduzione stesso) che potresti riutilizzare per la verifica formale.

Se si conoscono sia Python che C, è possibile utilizzare cython che converte la sintassi simile a Python in C. Viene utilizzato per scrivere estensioni CPython.