Well then you're going to be happy : there's a new Spark-to-C compiler. http://blog.adacore.com/spark-tetris-on-the-arduboy http://blog.adacore.com/spark-tetris

Well then you're going to be happy : there's a new Spark-to-C compiler. http://blog.adacore.com/spark-tetris-on-the-arduboy http://blog.adacore.com/spark-tetris-on-the-arduboy Maybe that's the one you're thinking about ? Also, I heard Rod Chapman (at the last AdaCore tech day) say they had great success using 'the' Ada-to-C compiler some years ago. Looks like AdaCore still have the code for it, not doing much with it. You might get the code if you ask nicely (maybe T.Taft directly now that he works for AdaCore) :-D. If you get any new idea on some combination of Spark, Ada and other tech, I'd send yannick moy an email :-D. Always helpful and insightful. If you plan on doing your borrow checker as some kind of new static analysis pass for Ada, I'd also look into libadalang, there's some great (open source !) progress there. I also played a lot with gnat2xml but I don't recommend : it works but it was painful... I also wondered some time ago about a Spark-to-rust compiler. But I'm waiting for my rust skills to improve first. Anyway, it's very strange to see rust every so often mentionned for embedded software. I get the interest for 'normal' unconstrained software. But after 10 years of large-scale real-time embedded-systems programming in Ada and I maybe faced once a memory safety bug that the borrow checker would have prevented. Mostly the bugs you get are constraint_errors (overflow, underflow, array bounds,...) most already caught by the type system at compile or static-analysis time. The rest are mostly 'real' bugs : logic or temporal. You never doubt of the state of the program when reading the code, such a lower cognitive load... Going back to C from time to time is so painful, especially, when you think of all the help you're missing. When in need of pointer go for not null access types, when in need for dynamic allocation go for controlled types (scoped deallocation) and storage pools... Everyone (except haskellers...) is missing on so much, it feels like living in the future where the compiler works (a lot !) for you. Sorry for the rant... By the way I found one of the ways to catch temporal errors (other than uninitialized variables that are caught) in Spark is to use an enumerated state variable and check it all the time (post/pre or in invariants). It's almost always a good idea anyway to have an explicit state instead of some 'nah none will call this code in such sequence...'. Also interesting : like functional programming or the borrow checker, or strong typing, Spark changes the way you think about your code. You think about how 'provable' your design and code is and it makes code more readable, simple. You can also just start with data flow annotations (also great for safety and security-critical code), makes reading code easier. I'll be looking out for your next dive back into Ada then !