title: High-level system language that compiles to c?
body: <p>I'm looking for a higher-level system language, if possible, suitable for formal verification, that compiles to standard C, so that it can be run cross-platform with (relatively) low overhead.</p>
  
  <p>The two most promising such languages I've stumbled during the past few days are:</p>
  
  <ol>
  <li><p>BitC - While the design goals of this language match my needs (it even supports the functional paradigm), it is in very unstable state, the documentation is out of date, and, generally, it seems like a very long shot for a real-world project.</p></li>
  <li><p>Lisaac - It supports Design-by-contract, which is very cool and has a relatively low performance overhead. However the website is dead, there hasn't been a new release since '08 and generally it seems the language is dead.</p></li>
  </ol>
  
  <p>I'd also like to note that it's not meant for a real-time system, so a GC or, generally, non-determinism (in the real-time sense), is not an issue.</p>
  
  <p>The project involves mainly audio processing, though it has to be cross-platform.</p>
  
  <p>I assume someone would point me to the obvious answer - "plain ol' C". While it is truly cross-platform and very effective, the code quantity would probably be greater.</p>
  
  <p>EDIT: I should clarify that I mean cross-platform AND cross-architecture. That is why I consider only languages, compiled to C in the first place, but if you can point me to another example, I'd be grateful :)</p>