Ten Years of Using SPARK to Build CubeSat Nano Satellites with Students
blog.adacore.com
blog.adacore.com
I agree C is not a generally safe language, but it can be done correctly. I'm not surprised that many cubesat satellite projects have failed due to software problems. Whatever language is chosen, these are still generally launched by students or those learning the ropes. Failure should be expected and using a very strict language will help, but is ultimately only a crutch. It comes with a lot of cognitive trade offs.
Not having an update mechanism period though? That's positively madness. Not having a fallback system in the event of systemic failure? Unheard of in real satellite systems. Bad things happen. Ada will not protect you against all classes of failure and will incur a very large development cost.
What happens in the real world? C. Even some mixed assembly and in the worst of worlds Java. What do I want to see? More Rust. Rust covers the worst of errors without much cognitive overhead, and zero runtime overhead. It's bare metal and very efficient. It's been in space and I guarantee more of it will be going to space.
Ahm, Rust is much worse than SPARK in case of covering errors, and its runtime overhead is no less than that of Ada.
>Not having a fallback system in the event of systemic failure? Unheard of in real satellite systems.
The bad thing about software errors is that fallback systems doesn't help with them. If your computer says not to turn on the thrusters until 100 meters below ground, you will crash. If you have a software-controlled stuff and software behaves badly — you are doomed, and Ada has a huge advantage here, that's why it's still used in aerospace.
Can you elaborate? It's not often that they see valid critiques of Rust on HN, and it would be interesting (to me at least) to add to the data bank.
Here's another post with some examples: https://blog.adacore.com/taking-on-a-challenge-in-spark
There's a good book, Building High Integrity Applications in SPARK, that goes through things in detail. It's a good read for any programming language user to mine for ideas or explore how similar problems could be solved in their language: https://www.cambridge.org/core/books/building-high-integrity...
Ehm, SPARK has a full proof capabilities, pretty much like you have in Coq (and SPARK integrates with Coq). With SPARK you can prove your code is correct, with Rust you can't, and there is nothing like Frama-C/SPARK available for rust.
In Ada12/SPARK14 you have statically checked Hoare triplets (in Ada contracts are ensured in runtime sometimes tho), you can ensure that your output array is sorted in the type system and prove it statically, you can ensure all sorts of invariants statically.
I like rust, but it's nowhere near proving correctness since it has neither dependent types (like F star/Low star` has), nor dedicated proof system (like Frama-C/SPARK). You can compare Rust to Ada, though Ada is pretty awesome two and have many features Rust lacks (contracts, subtypes, parametric modules).
This with a language that supports tasking, generics, and oop natively...
And proof on access types (pointers) are on the way.
Really amazing tech to work with.
Rust might seem like a big win compared to the average C or even C++ projects due to its memory-safety guarantees, but at the end of the day the only thing it has on Java or Python is protection from data races. It also has some type system features which enable writing robust code, but SPARK is in a different league.
"Failure should be expected and using a very strict language will help, but is ultimately only a crutch. It comes with a lot of cognitive trade offs."
The best study I ever saw doing comparisons put Ada at safer and cheaper to use for critical software:
http://archive.adaic.com/intro/ada-vs-c/cada_art.pdf
SPARK proves absence of certain kinds of problems that even experts run into. You can do that with static analyzers and such on subsets of C. They tend to cost way more than a SPARK Pro license. SPARK the language is also easier to learn than mastering C with all its dark corners. If not proof, they can also do contract-based, test generation and/or fuzzing with contracts as runtime checks. Will knock out tons of errors.
So, I think the evidence is against your claim so far. And, as to this:
"What happens in the real world? C."
COBOL, Excel, Visual Basic 6, C, C++, Java, and .NET all have piles of code out there. That mean any one being dominant proves its the best? Nah, that happens for social and economic reasons, esp when ecosystem is established. Especially for C. It's worth considering alternatives such as Ada/SPARK, Rust, and D.
I'm also for making the alternatives plug into and use C ecosystem nicely. Maybe even compile to it to leverage its tooling. When that happens, the alternative will strictly be better than C for being able to use all of its ecosystem strength with as little or much weaknesses as integrators want to bear.
From my understanding, most cubesats do not have propulsion. Can the software render them totally inoperable (other than draining power).
Is that true? If there was ever a group of people who knew, it would be here.
Another option is to only release your source code.
If you use the GNAT Community version, there is a runtime exception which states you don't have to release source if you just use the stdlib (something along those lines). If you use any of the Adacore libraries, then you are under the GPL.
If you get the commercial GNAT compiler, you can of course withhold your source.
I'm not an expert or lawyer, but I was told (not by Adacore) that is how it works.
At the end of the day, this makes Ada an excellent language that I can't use. Their customers seem to work on big ticket items like aircraft and aerospace where the pockets are deep. It's a shame too as I'd love to use it over C.
This example of integer overflow is also very common amongst C/C++ programmers. Almost nobody cares about overflows or 2gb boundaries. Nobody knows how to efficiently use adc ("add with carry") or how to check for it at compile-time. spark does it for you automatically.
> ... I would feel utterly incapable of constructing a good compiler for Ada.
Source: The School of Niklaus Wirth - "The Art of Simplicity"
Here's list of problems one would encounter in creating a compiler for VHDL:
Floating keywords. The versions of VHDL introduce and then drop keywords from keyword list. A custom lexer would solve that and our solution was exactly a custom lexer.
Overuse of single quote. The single quote starts character literal (as in '1'), the use of attribute (SOMETHING'ATTRIBUTE_OF(args)) and the use of value constructor (RECORD_TYPE'(arg1, arg2, arg3)). In the latter case it is possible to have something like REC'('1',2, true) which, as you can see, clashes with the character literal rule if lexer is not context-aware. We used separate lexer and parser with the fixed direction of data flow and we skipped that concrete pecularity.
Context-aware lexers are not unheard of for, I would guess, 20 years now and actually quite easy to construct right now. You can use monadic parser combinators which are breeze to work with in right language. I specifically implemented VHDL-AMS parser in Haskell and from start to complete parse of full test suite I spent about a month, part time. BTW, it was faster than ANTLR version in Java.
Other than these things outlined above, VHDL is more or less straightforward language, with complexity equal to Pascal. All these pesky attributes, interesting FOR loops, etc, can easily be translated into SSA and compiled and executed efficiently.
And, to conclude, Wirth was right. It was not possible to built good compiler for Ada in 1980-s. You are, on contrary, not right in your quote - it is quite possible to build good compiler for Ada (and pretty much anything) now, with wide range of goodness, from good error messages to optimizing away constants that are created with functions on arrays.
Rocket Labs posted their pricing publicly in 2015: https://www.rocketlabusa.com/news/updates/space-is-open-for-...
Question for those in the know about the orbital mechanics of these... How does one "register? for an orbit?" - get auth to launch something? Do you have to pay a body to monitor the object you place in orbit so it doesnt hit anything? Who is responsible for preventing collisions? Finally, given that the price is ~100K to get the cube sat up there, what is the total-cost-of-orbit for a cube sat?
I believe geostationary and geosynchronous orbits have some kind of bidding/registration, but for a lot of LEO it's generally free space.
NORAD tracks every object near the Earth that's over a certain size (a few cm). There's tens or hundreds of thousands and growing. It's operator responsibility to avoid collisions. The ISS, for example, will adjust its orbit slightly if they get a warning about debris passing too close.
Can't answer for economics, but Aerospace is still a small and tight knit industry. We all learn from each other and study failures. Deviating from the standards (such as the aforementioned unsanctioned launches is frowned upon).
Your mention of parasite cubesats is already implemented on some launches.
To keep their launch schedule, they (as a US company still) launched on an Indian based rocket to intentionally avoid the denial. This is strictly illegal under both international law (as having been denied a launch by their governing country), and US law (for being denied launch by a relevant governing agency).
Space launches is definitely a small industry still, but it's fairly cut throat and I would only describe it as 'tight knit' in that generally every launch provider has interacted with every other launch provider. They will absolutely attempt to undercut each other and ignore certain paperwork as long as the customer has given their word that it has/will be approved.
Imagine an LEO “cluster bomb” with many tungsten bomblets that just sent a cloud of shrapnel out indisriminate orbit level?
Is there any defense?