5 ms·
Looks great. One question though (and this isn't criticism of the research, but just about the presentation/intended audience): why would anyone who's been so '
by dataflow 5y ago
Looks great. One question though (and this isn't criticism of the research, but just about the presentation/intended audience): why would anyone who's been so 'stubborn' (as they say) so far about sticking with C finally have a change of heart because of this? They clearly prefer to write C themselves, otherwise they'd have already moved on, right? It's not like having a C++-to-C or Rust-to-C compiler would've changed the game for them.
- tluyben2 5y ago(not one of researchers but I submitted this because I like the research) I have not tried Rust for a while so this might have changed, but in the tiny embedded devices I work in, where your 'free' memory is for instance 24kb and the speed of the MCU is a few mhz, there really is only C/asm. You need to mess around with every single byte to make it fit and fast enough. There are surprisingly many of these MCU's around everywhere around us. And you (usually) cannot update their firmware remotely (or at all actually), so it's important it doesn't have massive bugs.
- dataflow 5y agoPeople say this all the time, and maybe it's just my naivete, but I just don't understand why at least something like C++ is not an option in embedded spaces. Sure you might need to avoid operator new() and exceptions or whatever, but you still have so much more power than in plain C even with half the language removed, and avoid so many of the C pitfalls just by that. I know people kept telling me you "need" C for a kernel... and I just ignored them and wrote drivers and even a basic from-scratch kernel in C++, and they all worked just fine, and with so much less pain than C. And honestly, if C++ somehow (I don't understand how, but let's say somehow) has too much overhead... why would another language compiled to C be any better? It just doesn't make sense to me.
- Animats 5y agoYou can use C++ on even an Arduino. In fact, the Arduino development development is full C++. You just have to stick to the non-Clib features.
- tluyben2 5y agoC++ is no issue but, to make very small binaries packed with the features we need, you need a lot of fiddling and the end it does not look like c++. Not to mention that most embedded devs (at least in Asian, Africa and eu embedded corps which make deployments of millions of mcu's, not home arduino users: there might be more of those) work mostly with C. I think most are waiting to skip a revolution to something like Rust but that does not fit yet. So this solution gives at least some handles to add verification. That said, there are more of these projects. I think there is an F* project too. > why would another language compiled to C be any better? It just doesn't make sense to me. It seems that the formalization in the article allows for very low level operation which you would use in C while not writing C. As said, sure you can do that in C++ but then you gain little or nothing. I have not tried this, only posted it because I would like for something robust like it to exist. Now we use Coq (or more recent idris) to write things and hand translate them to mcu asm/c.
- pjmlp 5y agoNot really, there are options available for those that care to look around. https://www.mikroe.com/mikropascal https://www.mikroe.com/mikropascal https://www.mikroe.com/mikrobasic https://www.mikroe.com/mikrobasic Mikroe is just one possible vendor, there are others.
- tluyben2 5y agoSure, you can: Forth works too. But C is the standard (in my world anyway) so it would be c++ or rust. C++ already is used but Rust I have not seen yet.
- pjmlp 5y agoSure but you worded it as universal condition, hence my remark. If anything, just to raise awareness for others. Even C++ alone is already an improvement, provided it isn't just C compiled with a C++ compiler, e.g. AUTOSAR.
- tluyben2 5y agoYep, I agree but we never could make that fit. When it fit, it was just compiled with a c++ compiler pretty much. But I have not met an experienced c++ embedded dev in my industries: all are c/asm because it is always the cheapest (and thus most underpowered) we can get away with given the consumption demands.
- kaba0 5y agoMessing around with every single byte is a property of low-level languages. There is absolutely nothing C does differently than C++ or Rust. Hell, it may even be slower due to not having proper abstraction powers and programmers thus lazily choose the easier route with eg. linked lists. Also, due to rust’s semantics it can get better optimizations due to no pointer aliasing.
- tluyben2 5y agoI will try it again then. What is your experience with it in very small devices? As I read online still, the binaries would not fit in the mcus we use. Maybe I am missing something there which has changed or I just missed. I would love to see a realistic (not hello world) example on a 32kb mcu. So with significant amount of function points (we do decryption, signing, otp generation, display driver, keyboard, and lot more and people told me and I read online this would not work well with Rust but this is maybe outdated or maybe the code will just look like C? I don't know examples of anything realistic): think that would turn me and more people.
- kaba0 5y agoIf binary size is that important, then there is even better options than C: Zig.
- tluyben2 5y agoWell, every 0.01$ counts for these components as orders are in the millions or 10s of millions. Everything that can be cut gets cut. And now lead times count as well as there are shortages and some factories have many waifers of these low spec ones to sell. I tried Zig on Linux and it is nice: any restricted embedded examples? I will try both Rust and zig when I get home to see if it could even work.
- gradschool 5y agoDevil's advocate question for a person who likes this research: What formal definition of a "program synthesizer" would exclude C compilers from being program synthesizers? Similarly, what precisely distinguishes C or any other programming language from a "specification" language?