7

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.

The two most promising such languages I've stumbled during the past few days are:

  1. 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.

  2. 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.

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.

The project involves mainly audio processing, though it has to be cross-platform.

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.

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 :)

K.Steff
  • 2,164
  • 3
  • 19
  • 25
  • 6
    Have you looked at C++? It (is|can be) a high level systems language. – Seth Carnegie Mar 20 '12 at 02:28
  • 2
    Yes, but the complexity introduced by C++ is, I feel, not worth the extra trouble. Plus, every compiler on this earth supports a different part of the language standards, and having, e.g. exceptions, is a mess. Same goes for RTTI and generally every feature that makes C++ higher level. – K.Steff Mar 20 '12 at 02:33
  • If you really just don't like C++, you might take a look at D which has a GC among other things and is less complex than C++. It's a lot less popular though and doesn't have as many libraries, but it can interop with C code like C++ can. Neither of those languages actually compile to C though, they compile to machine code. – Seth Carnegie Mar 20 '12 at 02:37
  • Yes, you're probably right about C++ and D. To be frank, I'm _scared_ by C++. Maybe it's just too much "Effective C++" I've read :) The issue of true cross-platform-ness remains for D, and C++ isn't really a good language for formal verification and/or formal specifications AFAIK – K.Steff Mar 20 '12 at 02:42
  • No language is more or less suited to formal specifications, just write your code to do what the specifications say no matter what language you use. And you say you need formal verification, but non-determinism isn't an issue? Again, I don't think any language is more or less suited to that really, until you get into languages like Haskell. I don't think something exactly like what you want is available currently. I guess it depends on the investment you can make to learn the language. And yeah, I have no idea about cross-platformness with D, I haven't really used it much, just read about it. – Seth Carnegie Mar 20 '12 at 02:44
  • You're making a valid point about non-determinism, I'll point out that I mean non-determinism from time perspective. As for the 'formal verification', I disagree - there are tools for C, while verification for C++ is considerably harder. As you have pointed out, Haskell, and many purely-functional languages would do a terrific job for that purpose. – K.Steff Mar 20 '12 at 02:55
  • 1
    Ok, well I hope you can find what you are looking for. – Seth Carnegie Mar 20 '12 at 03:02
  • 1
    possible duplicate of [Which general purpose programming languages/implementations compile to C](http://stackoverflow.com/questions/1721804/which-general-purpose-programming-languages-implementations-compile-to-c) – n. m. could be an AI Mar 20 '12 at 03:24
  • I can't read English since I just learn it less than a month. But maybe you can try to compile scheme or other lisp-like code to c. There are lots of compiler can do that. – madper Mar 20 '12 at 04:29
  • Seth, I heard that it is non-trivial to formally verify C++ code, and this explains to me why OP is looking for languages designed with verification in mind. – Artyom Shalkhakov Mar 20 '12 at 05:23
  • IIRC the Glasgow Haskell Compiler has a C backend. – Alexandre C. Mar 20 '12 at 08:01

2 Answers2

3

I think you may become interested in ATS. It compiles to C (actually it expresses and explains many C idioms and patterns from a formal type-theoretic perspective, it has even been proposed to prepare a book of sorts to show this -- if only we had more time...).

The project involves mainly audio processing, though it has to be cross-platform.

I don't know much about audio processing, I've been mainly doing some computer graphics stuff (mostly the basic things, just to try it out).

Also, I am not sure if ATS works on Windows (never tried that).

(Disclaimer: I've been working with ATS for some time. It is bulky and large language, and sometimes hard to use, but I very much liked the quality of programs I've been able to produce with it, for instance, see TEST subdirectory in GLES2 bindings for some realistic programs)

Artyom Shalkhakov
  • 1,101
  • 7
  • 14
  • +1, This is the closest answer yet to what I need, however from a first look it seems the C code generated is required to be compiled only by GCC, which, albeit running on many platforms, is not ubiquitously available. – K.Steff Mar 20 '12 at 12:38
  • @K.Steff, if you really need a language that compiles to C that can be compiled by *any* C compiler, then it's a problem. However, I think you could settle on some specific compilers (say GCC and Clang) that would suit your needs at this point. Then we could work together to make ATS compilable via Clang (I remember that C files *did* compile with Clang last time I tried, but there were some "missing" headers, so...). If you need some exotic platform/compiler, then please be more specific; maybe we can work it out as well. – Artyom Shalkhakov Mar 21 '12 at 03:33
2

The following doesn't strictly adhere to the requirements but I'd like to mention it anyway and it is too long for a comment:

Pypy's RPython can be translated to C. Here's a nice talk about it. It's been used to implement Smalltalk, JavaScript, Io, Scheme, Gameboy (with various degree of completeness), but you can write standalone programs in it. It is known mainly for its implementation of Python language that runs on Intel x86 (IA-32) and x86_64 platforms.

The translation process requires a capable C compiler. The toolchain provides means to infer various things about the code (used by the translation process itself) that you might repurpose for formal verification.

If you know both Python and C you could use cython that translates Python-like syntax to C. It is used to write CPython extensions.

jfs
  • 399,953
  • 195
  • 994
  • 1,670