Embedded - 158: Programming Is Too Difficult for Humans

Episode Date: June 28, 2016

Fabien Chouteau (@DesChips) of AdaCore (@AdaCoreCompany) spoke with us about theMake with Ada Programming Competition. Giveaway boards are GONE.  The Ada programming language (wiki) is interesting in that it was designed for safety critical embedded systems (actually designed, requirements doc and everything!). The Ada Information Clearinghouse has a nice list of tutorials and books as does the very helpful Make with Ada Getting Started page. Elecia's favorite was Inspirel's Ada on Cortex. Some neat projects in Ada that we mentioned on the show: Fabien's CNC Controller (with code in github) Tetris on a Smart Watch (with a formal proof via SPARK) Nano drone flight controller (with formal proof via SPARK) The platforms supported in the contest are on the Getting Started page but you can expand that by looking at the SVD files in the AdaCore drivers on github. (Also, SVD files are neat.) One of the platforms already supported is the Crazyflie nanodrone. 

Welcome to Embedded. I'm Elysia White with Christopher White. Our guest this week is Fabian Schutteau, and we are going to talk about Ada, the language, not the fruit or the lady. Instead, it will be Ada and ARM Cortex processors. Sounds interesting. If you downloaded the show right away and we didn't have any delays posting it and you do it right now, you might still be able to get a t-shirt. Otherwise, they are gone and I don't expect we'll see more

until I start pining for hoodies at the end of the year. Thank you to everyone who bought one. We do appreciate it. Hi Fabian, welcome to the show. Hi, thanks for having me. Could you tell us about yourself? Sure. So I'm a software engineer

at a company called AdaCore, and we are developing and maintaining the open-source Ada compiler called Dignat. And we have many other tools that we can talk about if you want. But that's our flagship, I would say.

And that's AdaCore, A-D-A-C-O-R-E. That's right. And G-N-A-T, like the fly. Yes. Just last week, we didn't spell fly bricks. And I feel like this week, we should just spell the whole show. Okay. Sounds good.

So we'll ask you a few lightning questions before we get to Ada. Yes. These are the ones that are short, and we want you to answer with short answers, and then maybe we'll talk about them more. Chris, you want to start? Start again? Again, yes, really. All right. Favorite processor of all time?

I would say the Leon 3 processor. It's used in the space industry. Maybe not very common, but yeah. For your day job, well, no, actually for your not your day job, well, no, actually for your not-day job, would you describe your activities as hacking, making, tinkering, or engineering? I would say engineering at work,

if that's your question, and maybe all of the above in my spare time. I try to be an engineer, yes. Yeah. That's, yeah. Let's see. Beach, mountain, or desert? Mountain.

What is your preferred programming language? Ada. That was kind of softball, wasn't it? Okay. Yes. The follow-up is, what language should be taught in the first university CS course? Ada.

Oh, really? Okay. Yes. Jumping in. Well, then I guess we should really get started with the whole Ada thing. Okay, let's go. So, Ada is a language. It's sort of based on Pascal.

I've never used it professionally. I never even used it in school. I'd only heard about it in school. We discussed it in an intro course, but it was only as Ada does this. You use it when you design avionics or bombs, sadly. Really, really high reliability systems. Yes, that's the main market for either but really it's a general purpose language it's very much if you know c or c++ it's it's really non-territory there's a lot of difference but it's an imperative language. You compile it to machine code

and it's very close to what you know, actually. Having read over a bit of an Ada reference in the last week or two, it wasn't tough to learn. I mean, sure, the syntax was different, but it wasn't that different. Yeah, a lot of people say that it's a difficult language to learn, and it's actually a very complex one.

If you look at all the features, there is object-oriented programming, there is even tasking embedded in the language. So overall, it's a complex language, but you can start very simple with very simple features that will help you, I think, improve the way you program. So what kind of things? What makes Ada worth learning? if we see programming as communication, like when you program, you talk to a lot of different people. You talk to the other engineers working on a project.

You're talking maybe with the designer of the system. And of course, you're talking with the compiler as well. And I think the best way to describe Ada is to say that the language will help you to talk with all those people. It will help you to describe what you want to say very precisely. And it will avoid some of the undefined behavior or very strange corner cases that you will find maybe on other technology. And yeah, we can go through some example of that. Yeah, how does language, I mean, some of those are design issues or mental human fallibility issues.

So I don't know how language would prevent me from shooting myself in the foot. So let's take a very basic example of what you can do in Ada. If you're working with pointers, so there's a small difference here. Pointers in Ada are called access, But that's not a big problem. For instance, if you're writing an interface, you can specify that you don't want a null pointer. And that's a lot in the design by contract paradigm, where you give a lot more information to the users of your interface,

or maybe the implementer, if you're writing specification, you can write some of the specification using the language. And so, for instance, you say, this algorithm, this function doesn't make sense if you pass a null pointer. So you say it in your interface. Okay, that sort of makes sense. I mean, I think about that as statics in C or privates

in C++. Is that the right sort of analog? Yes, I would say there's, so this not null pointer, that's one example, but there's a lot of other things in Ada that you can do. So for instance, one that I like a lot is the ability to define ranges for every type. So let's say you're writing a driver for a temperature sensor for instance there will be in the in the datasheet of this sensor you will have a value that says this sensor will not return a reading

above i don't know 200 degrees and never below minus 100 or something like that. With Ada, you can specify this in your type. You can define my type temperature is an integer between minus 100 and plus 200. And that's another way to communicate with the users of your driver because they don't have to go look into the data sheet for the sensor. They know that the temperature will always be between those two values. And I thought that was pretty interesting. Although, given some of the systems

I've worked on where the enums enumerate everything in C or C++. And with MISRA on, I end up not being able to combine enumerations with integers or other variable types. And so I felt like looking at the Ada types and the ranges that you had to give when declaring a type, it was sort of like I was enumerating the world. Like months and days couldn't be confused because they were enumerations. And in Ada, that was very easy to do and it didn't involve lots of lines of typing, which

you would have to do if you were enumerating in C and you were enumerating like 1 and 2 and 3. Yeah, and enumeration in Ada are not integers. It's not the same thing. That's very important as well. Yeah, I mean if you say that a month is November, it doesn't secretly underneath equal 10 or 11. It's always got to be November. You can't trick it. Yes, that's right. But we should also say that in Ada, you can, on one hand, have a very fine definition of your types,

of the logical view of your types, but you can also have a very precise definition of the implementation and the physical layouts of the types, but you can also have a very precise definition of the implementation and the physical layouts of the types. So that's why I think Ada is even a better low-level programming language than C. What do you mean by that? I mean, like a concrete example? I think what a great example is when you're

writing a device driver and you're working bare metal with let's say microcontroller and we have example of that. I can give you the links. You can with Ada you can really map your memory in the memory map

register. You can really precisely define there's a three bit field here and then there is a one bit and etc etc and you don't have to deal with shift and bit mask and all that nasty stuff for example The other aspect of it is if you have, for instance, a network protocol that is also defined at this kind of details, you will be able to precisely map your data to the memory, including dealing with NDNS, for instance. Okay, so networking, I can see how that would be useful, because then you wouldn't have to worry about different hardware platforms.

Exactly. But, you know, you actually mentioned microcontrollers, and when we talk about languages on the show sometimes, we talk about Python, but while I know it's for embedded, I don't really think about it as an embedded language primarily. Python? For embedded? Well, yeah. It's used on embedded. I know.

But I don't think it's for embedded. But Ada, part of the specification was for it to work in small systems. Really? Yes. Yeah, that was... So the language was designed to meet the DOD requirements and a lot of that was for embedded. And I think it's in the first line of the requirements.

They're mentioning embedded systems. Well, and that actually leads to a different tangent, which is there is a technical requirements document for the language. Yes, that's something very interesting. And I think it's quite unique for a programming language. So ADA was designed, I think a lot of people know that it was designed for the DoD.

It was supposed to be the one and only programming language for every project. And the way they started this project was to actually start from a set of requirements, which is probably the best thing you can do to write software, right? It's quite a good practice, and it's very uncommon for programming language. So there's this very interesting document. It's called Steelman. It's from 1976, I think.

And it's a set of requirements for a programming language. And so... And that's just... That's a general set of requirements, not for Ada specifically? Oh, no, it's written to define Ada. Yeah, at the time, Ada was not even in the design phase.

It was before Ada. So the process was to write the requirements, have a look at the existing languages and see if there's one language that will fulfill the requirements, have a look at the existing languages and see if there's one language that will fulfill the requirements. And they said no, there is nothing that's good enough. So we will start designing a new language. And there was actually a competition. There were four different languages and the one that we know that won this competition is the Ada that we know today.

What happened to the other three? That's a good question. I guess they're completely forgotten. I think the Ada right now is probably a mix of one or two of the language. It was very much a research process. And some people say that it was too much a research process. There was too many new features in the language. But yes.

Well, and this requirements document, which really isn't very long, but it does start out with the first point. The language shall provide generality only to the extent necessary to satisfy the needs of embedded computer applications. Such applications involve real-time control, self-diagnosis, input-output to non-standard peripheral devices, parallel processing, numeric computation, and file processing. So why are we all using C?

I don't know. It's like they designed this language for us. Yeah, that's the point. The reason why we use C, it's a very interesting question. There's a lot of reasons, I guess. Yes, this document is great for, I think, if you are into language design, it's a must. You have to look at it.

It'll be in the show notes. In general, it's very interesting to read that document. So it was designed to be an embedded language. And it has been, but then it kind of got moved up to more fully featured computers.

And now it is back to running on embedded Cortex-M ARM processors, in fact. Yes. So as I said, the language evolved from the first version of 1983. The last version is 2012. And there's a lot of stuff. It's like C++. It's a very complex language, including the tasking part, which is really something special as well. But you can still control the features that you want to use.

And there's still inside this very complex language, there's still a very simple one that doesn't require any runtime support that's very efficient for embedded. And that's what we are trying to... It was never gone completely. It's really a language that is used to, it's never, it was never gone completely. It's really a language that is used in this niche market of aerospace and defense and railway, but we are trying to bring it back to the more broad audience, I guess.

One of the things that I have read about Ada being better than C is that pointers don't exist, or they exist in a very different format, a much safer one. But how do you get to processor registers without using pointers? How do you actually deal with memory mapped I.O.? So about pointers, it's true that there is pointers in Ada, of course, because it's a very useful technique

for programming. The other thing we can say is that it's easier if you want to program without pointers in Ada. If we're talking about C, it's almost impossible to not use pointer. About the memory map register, when you define a variable in Ada,

you have the option to define its address statically at compile time. So you say, I have an integer, and its address is, and you put the address. So that's how we do memory map register. And actually, there's a good example of that. We have a project, a few device driver for the SCM32F4. And there's a few example of memory map register. So I guess we can put a link if you want to have a look at that. Sure, we can do that. I'll add a note here.

The STM F4, remind me, what kind of processor is that? That's a, well, there's a different, different version of the STM32, but we are talking about mostly the STM32F4, which is an

ARM Cortex-M with a floating point unit. Single precision, I think. Okay. So,

that's sort of on the beefy end, but it's a very, very popular processor right now. Yes, there are people using Ada for AVR, for instance, 8-bit microcontrollers. Really? Yes. This is a shocking episode to me, just to be a part of.

Why? Why is that so surprising? Well, because my impression of Ada is it's a very big, full-featured language akin to C++. And, well, I guess C++ is on 8-bits too, but as soon as you go 8-bit, I start getting, why aren't you doing everything in assembly in C? Well, and there's still some,

like in 8-bit C++, you do not get to have the whole standard template library. Right, right, right. And Ada on 8-bit C++, you do not get to have the whole standard template library. And Ada on 8-bit, also, you do not get all the features. That's right.

You probably wouldn't have tasking. No, tasking is going to be difficult. But the M4F would totally have tasking. Sure. Yes, we do have tasking for that. And we can talk a little bit about tasking, if you want, on Ada. Yeah. So the tasking system in the full language is very complicated.

It's very complex. We have features to create tasks, to synchronize tasks, to communicate between them. And so that's very big and complex. And it's not very appropriate for microcontrollers or even for real-time application. So in ADA, there is a profile. So a profile is a set of restrictions on the language. And this profile is designed to bring the Ada tasking features to a real-time and small resources environment. So it's called the Ravenscar profile.

And basically you will have to know the number of tasks at compile time, but you still have the nice features of communication between tasks using what's called protected objects. You can see protected objects as it's like mutexes but inside the language so it's impossible to make a mistake and within the Ravenscar profile you actually have a nice property of you are sure not to have any deadlocks because we use the priority inheritance algorithm. So it's like, I like to say,

it's like having an RTOS embedded in your language. With certain restrictions, you said you had to know the number of tasks ahead of time. Is that the maximum number? Can you dynamically create and destroy them? Or is it, okay, there's five, and I instantiate five at init time, and that the maximum number? Can you dynamically create and destroy them? Or is it, okay, there's five and I instantiate five at init time and that's... No, you cannot allocate tasks live. You know the number of tasks that will run in your software at compile time.

The other restrictions are inside the protected objects. There is this construct, it's called an entry. So basically when a task is calling a procedure for a protected object, there might be a condition for that protected object. So let's say we are implementing a circular buffer and the entry could be, I want to stop running that task if the buffer is full because I cannot put any more data inside. That's one thing that you can do in Ravenscar, but you are limited by the number of entries for that protected object.

So you've mentioned Ravenscar twice. Yes. Is it Ravenscar or Ravenscar? Oh, sorry. No, no, it's not you. It's named after the... There's an English village or is it a city I don't know

oh there's a railway system and there's Yorkshire okay subset of aided tasking features

I think there was a meeting there and that's where they defined this profile and so there you go

that's the name okay so Ravenscar is what you use to do to specify how much of the real-time operating system you want to use.

Yes. And it's a set of restrictions. So basically you define a subset of the tasking in Ada. And what's great about it, it's portable. It's part of the language. So, for instance, if you have a Ravenscar application, you can run it bare metal using our runtime that we provide, for instance, for the M4. Or you can run it on an RTOS like VXWorks.

Or you can use the same application on Linux, for instance, if you want. So that's also a great portability feature of Ada. I have one in the weeds question. You mentioned do you have a runtime to support this on the M4?

Do you take advantage of the memory protection unit that's on some of those chips? No, we don't. That's because of the tasking scheme of Ada. A task in Ada is more like a thread than a process. There is no memory separation between the different tasks. That's why we don't really,

we don't need the memory protection. Well, it still exists for, like ThreadX can use it and smaller lightweight RTOSes. So it might be something to look at. It's not as heavyweight as like a full-featured process MMU. You can mark pages and a few sections to be off-limits. To be more precise, we don't use it because it's not defined

in the language. For instance, we have a customer that wanted to do a separation between high-reallability tasks and some other that were just logging or whatever. And they implemented on top of our runtime,

the memory protection for that. Okay, cool. So, yeah. Okay. I want to ask more about Ada, but I also want to make sure we give away the boards that you have.

So let's skip the Ada questions for a little bit and go to... We're bribing you to learn this language. Where we is AdaCore. I have nothing to do with it, really. Can you tell us about the Make with Ada project? A competition, contest, thingy-bob? So Make with ADA started as a blog post series

that me and my colleague Raphael did. So we have a small number of fun projects and the idea is to bring ADA outside of the niche market of

aerospace and defense and to show that it's also a good language for hacking and making. And so the Make with Ada contest is like the next step of that. And we are inviting all the developers, hackers, makers, engineers to try Ada by themselves. So we are organizing a competition. It's on makewithada.org. And the rules for the contest are writing embedded projects in Ada, running on either the Cortex-M or Cortex-R platform.

And you will be judged on four criteria, which are the open, dependable, collaborative, and inventive criteria for your project. I hadn't noticed the collaborative. What do you mean by that? So the criteria come from, it's actually what we define as the core value of AdaCore. And we try to map that to the competition. So collaborative for us, it means that you are bringing something to the community. So either you're working with other people

or you're making sure that your project has a nice interface so that people can reuse it. These kind of things. There's more detail on the website. Yeah, there was a lot more detail. Yes. But we should mention some prizes are available. First place is 5,000 euros, which is $5,600 for those of you unwilling to look up the math yourself.

It is right now. It is. Yeah. See you in a week. The conversion is just an indication. The prize will be in euro at the end. Second place is 2,000 euro. Third place is 1,000 euro.

And you have some special prizes. Could you tell us about those? Yes. So there is two special prizes that we call. The first one is the Robert Dewar special prizes. Robert was one of the founders of AdaCore and he was very much involved in the Ada community. And so these special prizes will be for the best project in the dependable criteria.

So we are talking about software quality here. It means, do you have testing for your project? Are you using formal methods? Are you doing code coverage? Or do you have specification? This kind of stuff. The second special prize is named after Lady Ada Loveless. And it's for the most inventive project.

And for those two prizes, the prize are one CrazyFly 2.0 nanodrone. So the CrazyFly, I didn't even know about this last week, or I would have asked our guest last week about it. Yes, I heard you. it's pretty similar i would say so it's a it's a small drone um quadcopter quadcopter palm size that you can program and it's 180 ish on seed studio and yet you can you can program it however you want. This one doesn't include Lego bricks. No, it's not. But it's very interesting.

I don't know if the... What's the name of the company that was on the show last week? Flybricks. Okay. So I don't know if Flybricks is open source, open hardware, etc. It is. It is? Okay. So it's the same for CrazyFly.

And the CrazyFly is used a lot in the research and academia, I think. It's a great platform for hacking and working on collaboration between drones. Swarms. We're going to get swarms soon. Right. And that is one of the platforms, I mean, this is sort of a chicken and egg problem. That's one of the prizes, but that's also one of the platforms people could base their entry on.

Yes, that's right. So we have a few platforms that we support, let's say, out of the box. We have the few platforms that we support, let's say, out of the box. We have the CrazyFly. There is four STM32 discovery boards. You can find the list on the website. And we have also the PebbleTime smartwatch. But of course, if you want to work on another Cortex-M board, you can write support for it. We have a blog post that will explain how to do that.

And that would be a great contribution for the competition. Adding points to the collaborative column. Absolutely. Okay, so what if I don't have one of those boards? Are you giving out some boards today boards are you giving out some boards today are you giving out some boards one of us is

I'm not yeah I guess we are yes sure we are so I contacted you to ask if you were willing to talk about the competition on the show and maybe organize a giveaway. So do you want to explain?

Yes, three boards. I guess what we can do is we can select three winners and they will ask us which one of the platforms they want out of the four discovery boards, which one of the platforms they want out of the four discovery boards, which one they prefer. The Crazy Fly and Pebble are off the table, but the four different discovery boards you can choose from.

And I don't normally do this first three people contest because my personal podcast backlog is very long. But this is a timed competition. It started last week. Well, it started June 20th? Yes.

And it goes until August. When does it end? I think it's the last day of September. Okay. So you do want these boards soon so you can get started. So we are going to do a first three people but in order to fend off the people who hoard boards like i do um just you know when you enter just email and say i plan to enter the contest if i get the board uh the make with contest, and then I will update the show notes when all of the boards are gone.

So if you, otherwise you can, yeah. So email if you want a board. But don't lie. But don't lie. No, that's karmically bad. Go enter the contest. Yeah. Make something.

Make something. And you know, I would often say, well, tell me what you're going to make. But I'm not even going to put that restriction on this time. But you can. But you can, yeah. Of course you can. You don't have to. Well, Chris and I are going to have a show, it's just us. So if you tell us what you're going to make, we'll probably talk about it on the show.

All right. Okay, so yeah, you got that. First three people to tell me they're going to enter the contest if you get a board. And then I will email you if you win and then I will forward your email address over to Fabian who will get your address and ship you a board. And I should mention as well that for the first people to

register their project on the website, they will get a t-shirt. And I think we have about 100 to distribute. Oh, excellent. Yeah. So you don't even have to contact me for that. You can do,

or you might be able to get a board and a t-shirt. Yeah, that would be great. So. All right. Okay. So this contest sounds very cool. Do I need to buy Ada? No.

Do I need to buy AdaCore's NAT Pro in order to win? Nope. Of course, that's the right answer. Yeah. Gnat is an open source compiler. So it's based on GCC. And so the sources are available in the GCC branch and the GCC repository. So you can start with that.

But of course, we distribute a public version of the compiler and that we recommend if you want to start the project. It's on our libre.adacore.com website and you will find the links in the Getting Started page of the competition as well. So the Make with Ada Getting Started page starts with the video on how to install things, which you needn't turn your sound up on that

because there is no sound. No. But then after that, it has a lot of stuff like tutorials and lists of ideas for projects and boards. So the Getting Started page, don't just stop with this. Go past the video and scroll down because it had a lot of good stuff. Speaking of tutorials, I went through the Inspirels Ada on Cortex-M book.

And it went through the, it was really cool because it was, here's Ada, but also here was a lot of how embedded systems work. It was a neat's Ada, but also here was a lot of how embedded systems work. It was a neat tutorial on both. And then there were lots of things about linkers, which I kept cringing about, but I thought it was a really good education. Why were you cringing about it? They were solving some of Ada's mapping interestingness? That's the part that I don't like about this book.

It's a very good introduction, but this part is not very... It's not how I would do memory mapping in Ada. That's not the right way. But then it also talked about state machines and how they work for embedded systems and about hardware abstraction layers. And it kind of worked this all in with, here are four different Cortex boards and here's how Ada works. And it was just, it was a nice read, actually.

I was happy. But then, yes, you have a different way of doing the mapping and the board support package layer of things. Yes, we have a, it's kind of a new project. the mapping and the board support package layer of things? Yes, we have a... It's kind of a new project. My colleague, Jerome, works on that. So there's this hardware description format from ARM. It's called SVD. And basically, it's just an XML file

with descriptions of peripherals and registers where are they mapped in memory, what fields are inside, etc. And we use that hardware description to generate mapping in Ada. And again, I can give you a link to an example of that. But it's great because that's very the annoying part of writing device driver is to map to the hardware. And with that, it's all automated. And you can, as I said earlier, you can stop messing around with bit shifts and mask

and all that stuff. This is the kind of thing that I've been wanting for a long time in Embedded is stop making us rebuild the world from scratch every time a new project comes along. And this is the kind of thing I've been hoping somebody would build. So it's kind of exciting to hear that oh, somebody's working on this. Well, that's not an Ada-specific thing. No, it isn't. That is an ARM Cortex CMSIS family of features. Actually, I think that ARM distributes C code generator for that format.

The problem is that only in Ada you have this very fine control of the representation of your types. And only in Ada it is really useful to have this definition. Do you find that working in Ada makes you a better C programmer? Because I do think you're often a C programmer if I've read your LinkedIn. Yes. So at work, I'm working on both the Ravenska runtime that we discussed earlier. That's 100% in Ada.

And on the other hand, I'm also working on the QEMU and we have an emulator product based on that. So QEMU, it's C. It's very, I'm sorry to say, a nasty use of C. So yes, I do have to deal with it. Does it make me a better C programmer? I don't know.

One of the things that I do, for instance, is that I will never use an integer or a pointer as a Boolean value, for instance. That's something that's completely out of question in Ada. And you can go back to... I can read it like, if pointer, that doesn't make sense. If pointer is different than null, that's okay for me. Okay.

Yeah, I've heard Andre rant about that as well. Yeah, I guess it's in a lot of programming style and programming guides, but it's not enforced by the language. So you will always find somebody that's that's going to use use that sure i found that the way that it framed everything the the type checking made me think about some of my c differently that i should be doing more of that. And while in the code, nothing bad happens if it's out of range, really the calling code should never give me things out of range and I should be doing more error checking on that. So it was one of the things that reading through Ada

made me think more about. Is this what's meant by programming by contract? That's something I've heard associated with Ada a lot. Yes. But I don't really know what it means exactly. So actually, even in C, you are programming by contract. Just violating constantly. Yeah, and also you have less expression power. So when you're writing a function,

like if we say, if we talk about the device driver for the temperature sensor you will have a contract that you contract with the user of your interface that you return an integer value that's a contract so the user doesn't expect a floating point or pointer pointer, etc. So there's already in C, C++, there's already a contract. Through the header file, through the function prototype in the header file. That's the contract you're talking about. Yes, exactly.

The API, the signature of your function. With Ada, because of the type system, you can specify a lot more things. You can express a lot more. So that's why it's better at contract-based programming. And there's also, in the last version of Ada, there's the precondition and postconditions. So you can have very high-level specification about your program.

So for instance, if we are talking about the temperature sensor driver, you can say the precondition of reading the temperature is that the device is initialized. And this is also embedded in the language. So it will be checked at compile time. If you want to, it will also be checked at runtime. You can specify it. So it's like having asserts only embedded in the language. And you can also have, for instance, type invariant, which will give constant properties about a given type that you that you have so like mutable and immutable things in

Swift or Objective-C I would say it's it's more it's higher level than that so for instance if you have you're implementing a list so the implementation is private. You don't show it to the user of this library, let's say. You can specify a type invariant that the list will always be sorted. Okay, wow. These kind of things.

Wow, okay, yeah. Along with contracts, you often hear Ada used with Spark. Yes. What is Spark? So Spark with a K, it's two things. First, it's a subset of the Ada language. So mostly it removes a good chunk of the tasking and the pointers. And there's also a tool that will perform formal proof,

so mathematical proof and reasoning about your program. And what you get from that is the first level is you can get proof that there will be no runtime error on your program. So that includes no division by zero, no integer overflow, or no out-of-band access on arrays. So that's already something very, very powerful. But this is static. I mean, you do this at compile time. Yeah, sorry, that's a static tool. So it will analyze your program

and give you the proof or will try to prove the properties. Maybe it's not possible to prove because there's something wrong in your program. But once the tool returns and saying it's okay, you're 100% sure that there is no runtime error on your program. And that's the first step. But it's already very powerful because, for instance,

if you say there is no possible buffer overflow on your program, that's a very, very powerful assumption, right? And the next step is to use the precondition and the past conditions. And you will also be able to prove that those conditions are met. Like what I said about the list that will be sorted, the tool will try to prove that every time you manipulate your list, you will always return a sorted list. How the hell did they do that? Well, it's kind of like if you turned

all of the MISRA, if you checked all the MISRA boxes and you turned PCLint into, oh my god, tell me every little thing. Well, it seems like it has to execute code and do speculative things to see that. So I'm not going to talk about implementation. Yeah, that's fine.

It's really out of my range. I'm mostly expressing surprise. It's math, basically. You're proving properties. And you're talking about lint. I think it's another level. Oh, yeah. No, it's like super lint,

like super duper lint. Yeah. We have something closer to lint. We call it Codepier. And we would define it more as a bug finder. Like, I will do as best as I can to find bugs in your code. But with Spark, you have the 100% mathematical proof that there is no error in your program. And that sounds brilliant.

It sounds awesome. It sounds all sorts of fantastic. But the downside is... There has to be a downside. There is no free lunch. Where is my free lunch? You have to tell it all this stuff. I mean, you can't just say,

give me an integer between zero and 12 and we'll call that a month you have to specify the months and then every time you use the months you have to make sure they're specified correctly in all the spots because it's a type you get some of that for free but you still have to do all the little checkboxes. You have to do the kinds of planning and bookkeeping that you should be doing normally, but the language enforces it.

Well, Spark enforces it more than Ada does. Ada enforces it more than C does. And C enforces it more than Punchbox. Monkeys? Assembler. Yes, so the first level,

the proof that there is no runtime error, that's something that you would basically try to achieve by unit testing, right? And with Spark, if you do it right, you can remove all your unit testing, basically. So the time you spend making your program correct, you will not spend it writing tests. And the other aspect is that with using the precondition, the postcondition, and all the contract-based feature of ADA, you are

also writing the specifications of your software and sometimes the low-level specification can be written in Spark, actually. I would like to join your religion.

So far, you're doing an excellent job of selling this to me. Oh, thank you. There was a very nice comment on one of my Make With Ada projects on the smartwatch where I use Spark, actually. It's a project from two of my colleagues, Yannick and Tristan. They did Tetris in Spark. So on a Pebble.

Yeah. And then I made it run on the smartwatch, yes. And there was this comment. So the guy was saying, this project seems to come from another dimension where we use the same programming language the API is well defined etc etc

but no we are from this world and so there are some really interesting examples you have this Tetris on a smartwatch there's a nano drone that

it seems like Spark is saying you can't crash the drone. I mean, that's what it all comes down to, which is crazy. That's a long, long stretch, but I can explain the drone. So that was a project made by an intern at AdaCore, Anthony. He's now working full-time. The idea was to take the flight controller of the CrazyFly, which is written in C, to translate it to Ada, and then to choose a very critical part of the project. And in that case, it was the stabilization algorithm

and to prove the absence of runtime error with Spark. And so, yeah, saying that the drone will not crash is, of course, a big stretch. Yeah. It will do what you intended it to do in the code,

and perhaps you didn't realize what you intended it to do when you wrote the code perhaps you didn't realize what you intended it to do when you wrote the code. Exactly. That's the whole point of requirements and specifications. And you did another project recently, a CNC controller. Can you tell us about it? Yes, that was the last project in the Make with Ada blog post series.

So it's a small CNC machine made out of DVD drives and it's just what's called a pen plotter. So you can move a small pen in three axes to draw on a small piece of paper. And I did the controlling software. So there's the embedded parts inside the microcontroller. It's in Ada. And there's also the host application that will simulate first the movement of the machine and then send the code to be run on the small machine. And this was all done in Ada. Does it do Spark as well? No, I didn't use Spark for this one.

Okay. That was, I could, but no. Well, I mean, it's good to know that there is difference because Spark does require a higher level of commitment to writing it all down and all the details. Yeah, so Spark, it's probably not for the entire project. So for instance, in the CrazyFly, we decided that with Anthony,

we decided that the stabilization algorithm was a great place to use Spark because it's only math and the tool can pretty much easily work with those operations. But sometimes writing tests is more effective than using Spark. Sometimes using Spark is more effective. You have to decide at some point. Yeah, so you'd focus on the core algorithms perhaps. Yes.

Like for the Tetris, only the game system is checked with Spark and when there's the interface with the buttons and the screen on the watch, there's no Spark here. Yeah, that makes sense. I mean, interacting with humans is so hard. So you have, I guess one of the things I'm trying to get to is there's this contest.

It's in this language that not everybody knows, but there is a lot of stuff already done and it's already open source and people can go and look at examples and it's not that hard. Yes, that's the point. Well, it's an outreach contest. You're saying that from the beginning that you want to get people involved in learning it so it's not like hey, experts only. Yeah, sure. The whole idea with this content is we want

new people to try Ada and try to bring more people to this community. And I emailed one of the judges, our friend Jack Gansel, where it's like totally name dropping there. And I asked what he was excited about with the contest. And he said, oh, I might as well just read this. One of the most interesting developments is Ada is that it's now being used on MCUs like the Cortex-M.

And we should explore that so many engineers adamantly argue that it's only available for big processors. One of the make with Ada platforms is Seed's crazy flight drone, which weighs only 27 grams, yet has 32 bitters on board, plus lots of sensors. And then later in the email, he says, this is very cool. Ada is very cool because we talked to him about being a grown-up engineer and doing all the prep work and being careful.

And I think Ada really puts you in that mindset more than C, where you can hack something together and that's okay. Do you agree with that, Fabian? Yes, I do. I think there's a lot of myths about Ada, like Jack said, some people think it's only for mainframe for whatever reason, or some people think it's only for mainframe for whatever reason, or some people think it's dead or this kind of stuff. I think that another myth is that it's a very difficult language to use

because there will be a lot of compiler error. And the reason is, it's by design. We want the compiler to check as many things as possible. And sometimes it's painful to have all those errors on your program. Like you want to say no. You want to say to the compiler, you're too stupid, I'm better than you. But you have to realize that maybe programming is something too difficult for humans

and we should listen to our tools. And you know, when the compiler says signed, unsigned, comparison mismatch, and you're like, oh, that doesn't matter. It's fine. It's fine. It's fine until some point when it isn't. And then it's so not fine.

Exactly. One advice that I like to give for people trying ADA is that every time they get a compiler error, they should try to think about what would happen in another language. If that error is not catched right now when you're compiling, what's going to happen? And usually it means painful debugging on the target for hours and hours. Or, yeah, maybe not hours, but a painful amount of time. Probably hours. Probably hours.

Maybe weeks. If you had time and you weren't an organizer, what projects would you be considering entering? So there's, as you said, there's a list in the getting started page of a few examples that we would like to see. And I wrote that list so you can have a look. I think what would be interesting is to add support for the Arduino and the Adafruit boards.

And I would like to see the equivalent of the Arduino interface with the digital read, digital write, to have someone maybe trying to define a standard Arduino interface in Ada. That would be cool. Do you have any projects, Christopher? I have all the projects. You know the projects I have yeah but would are there any that

you'd be thinking about learning a new language with um any of the drone experimentation I was thinking of doing might as well I think the how

do you call that the dodeca yeah would be a great not a serious project but yes um but yeah any of that where you know there's complicated math going on,

I think that's where I would say, okay, this is where I would want to apply this. Because doing that sort of thing in C is always really painful. Because you do skip steps and you do take liberties with language because you can and more formal things like control systems seem like well suited to being proven or at least better locked down. Sorry, there's a small

detail that I forgot to mention but we have fixed point support embedded in the language which is pretty cool for micro controllers as well. Yeah, but then you're giving away a Cortex-M4F. You don't need a fixed point. You don't.

Okay. We'll take it out. No fixed point for you. Just for me. I think that if I was going to enter, I would probably redo my North Star project. Oh, that'd be good, yeah. Because I've done it on two platforms already, and I thoroughly understand the code. And hooking an LED to an inertial system so that you can see how acceleration works and how gyros work and how magnetometers work in the real world, I guess that would let me look more

at the language. And so that's the one I would be tempted to enter, although I don't intend to enter because I would rather read other people's at this point. And because I have other projects going on. But I think everybody else should enter so that I can read their projects. Yeah, that works. Good idea. And remember, you can cross-post with Hackaday, so if

you're thinking what you need is some assistive technology or whatever their next group of sections is, go ahead, have fun. It'll be cool. We'll all look forward to it. I think that about covers it. I think we're about out of time.

Christopher, do you have any other questions? I have only 12 questions. Okay, go ahead. I do have a couple. Wait a minute, don't you have to specify their inputs first? No, this is English, which is worse than C. First of all, how did you come to learn about and use Ada? Where did you get exposed to it?

There was a short introduction in my engineering school. And then I was introduced to AdaCore and was more than Ada. And that's where I ended up using Ada. Okay. And we touched on this earlier, and I think you kind of answered it throughout the show, but I am curious if you have a more compact answer for why aren't more people using it?

Why hasn't it sort of been more popular? I think it's because of a very, very bad start. At the beginning, the tools were pretty bad. Slow compilers producing very inefficient code. And everything was closed. There was no open source platform available or even a low-cost compiler for people to use Ada. And so I think it's really because of a very bad start.

Are the compilers better now? I mean, is there much of a speed penalty for using Ada instead of C? There's a few. That's another myth about Ada. There is many runtime checks that are defined by the language. So, for instance, if you want to check

that the value is indeed within the range that you specified, there you want to check that the value is indeed within the range that you specified, there will be a check and that's, of course, a penalty. But you can always remove every check. And the point is you want to have the checks enabled when you debug because it's better to catch a buffer overflow when you debug than smashing your stack and having the code jumping everywhere and then when you are in production you will remove probably remove all the checks but that's up to it's it's a system and a safety concern concern. So an example is,

for instance, if you're, yeah, let's take a good example for you, Chris. If you're driving a very powerful laser and you define the driver

and you specify that the value for the power of the laser should be between zero and 100. And somebody uses your interface but

puts, let's say, 10,000 for the power argument. What would you do? You have the choice of disabling all the checks and praying that everything will be fine or you can have a check and

this will raise an exception and you can decide what to do. Probably you want to turn off everything and reset the board. That's up to you. Well, then I think we are out of questions. I'm not really. There's so much more to talk about with Ada. It was pretty fascinating.

But I think we are out of time. So Fabian, do you have any last thoughts you'd like to leave us with? I would say just give it a try. Start a small project and try by yourself. See if it's good for you. It's always a good way to start. Especially, yeah, definitely start with a small project

and don't try to do your next company based on this podcast. But there are also some really nice, more fully featured projects out there you can read. Yeah. And Ada was a reasonably legible language, I thought. They're all getting worse, so Ada didn't seem that bad to me when I looked at some of the example code compared to, say, Swift,

which is supposed to be nice, but it's hard to read. Yeah, the readability part is really strange because there's only Ada, in my opinion, that's addressing the fact that we read code more than we write code. Yeah. Yeah. All right. My guest has been Fabian Achuto, software engineer at AdaCore.

Thank you so much for being here and for giving out some hardware. Thank you also to Christopher for producing and co-hosting. And of course, thank you for listening. You can enter to win if you hit the contact link and say you would enter the Make With Ada contest if only you had a board. The show notes will tell you if they've all been given out. You can also email us show at embedded.fm. Or if you'd just like to say hello, that link and that email will do you. And now a final thought. Oh, let's just go with Ada Lovelace because you've been waiting the whole time.

The analytical engine has no pretensions whatsoever to originate anything. It can do whatever we know how to order it to perform. It can follow analysis, but it has no power of anticipating any analytical relations or truth. Its province is to assist us to making available what we are already acquainted with. Embedded FM is an independently produced radio show that focuses on the many aspects of engineering. It is a production of Logical Elegance, an embedded software consulting company in California. If there are advertisements in the show, we did not put them there and do not receive any revenue from them. At this time, our sole sponsor remains Logical Elegance.