I think the constant evangelism of Rust enthusiasts - “let’s rewrite X in Rust!” - gets to some HN users, which in turn leads to (often times unfair) downvoting of Rust-related comments.
The account posting it belongs to an employee of kubos. Usually that would be tolerated around here, if it's on-topic and they were to add something akin to "full disclosure: I work for this company". You could debate if it's relevent enough to the article, but either way it'll seem way too close to spam with just that one-liner.
You know what would be really interesting in the future for SpaceX - would be to have 'parasitic' launch capabilities whereby it could eject cube sats along its path as needed - like a cluster-bomb ejects bomblets.
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?
Private spacecraft are under the authority of the government from which the organization originates in. For example, Swarm got in serious trouble with the FCC when they launched on an Indian rocket without FCC authorization.
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.
The reason Swarm got in trouble is that they were launching smaller than cubesats, had applied for a launch license, and had it denied because of the inability to track the payloads.
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.
What would be the pre-emptive-defensive action an authoritative body could take, should a rogue element launch tungsten “dice” into the orbital paths of *anything.
Imagine an LEO “cluster bomb” with many tungsten bomblets that just sent a cloud of shrapnel out indisriminate orbit level?
The license prohibits you from using Adacore's tools unless the software you release is also GPL, right? I thought that was the case so I never really bothered with Ada.
Is that true? If there was ever a group of people who knew, it would be here.
Adacore releases a GCC/GNAT compiler on their website that has no runtime library exception. You can build your own GCC/GNAT (not difficult) or install from another source (e.g. your distro's repo).
Another option is to only release your source code.
I looked into this as well recently and came to the same conclusion:
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.
The Ada standard library is massive and is included in the exception. There are "internal" "GNAT specific" packages which you can include in your project but there are not really any you need or would use in a general sense - there are even warnings you get at compile-time telling you that you are using something GNAT specific and are prefixed with GNAT.* instead of Ada.
"massive" meaning a ~300 MB compressed download, compared to a 20mb C++ with stdlib. it's even more more massive than the biggest professional lisp packages. Only Microsoft and Apple Tools can compete with that kind of massiveness, but they ship a lot of crap with it. Ada/Spark is an extremely nice and easy to use framework (if you forget the python crap that comes with it), and I would hire any Spark or ATS or F* programmer over a C++ or Java programmer in a minute. no questions asked.
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.
Thanks. I always see SPARK the Ada dialect and tooling all caps, and Spark the JVM distributed computing framework with just the first letter capitalized, and I figure there are probably a lot of readers interested in one and not the other.
The author states that many of the other cubesats were dead on arrival due to software bugs. Given these things cost so much, doesn’t it make sense to put an update framework into these?
From my understanding, most cubesats do not have propulsion. Can the software render them totally inoperable (other than draining power).
Yes, many cubesats need attitude control to point solar panels at the sun. This is usually done entirely in software. By the time you know there is a problem, your spacecraft is probably dead. You probably only have 60-90 minutes of battery life.
With no possibility of updating software doesn’t that make the cubesats vulnerable to potential hijacking via vulnerabilities in the software? If this is the case, the cubesat could become a particularly difficult to address part of a botnet if it can be made to run code arbitrary code.
Whelp, I was a VTC student and Professor Chapin was positively an amazing professor. I wouldn't be nearly the software developer I am without him. With that being said. I would never, ever, use Ada for a non-academic project including those for embedded systems headed to space.
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.
>Rust covers the worst of errors without much cognitive overhead, and zero runtime overhead.
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.
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...
>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.
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).
And, even if you don't go 'full platinum level proof' (proof of all the High-Level specs of your software) in SPARK you can still enjoy, without too much effort:
- proof of no read access to uninitialized variables
- proof of absence of runtime errors (overflow, underflow, array out of bound, incorrect conversion...)
- proof of type predicates/invariants, asserts, pre/post conditions...
- Less known, you can specify and verify 'data provenance' with 'this function's result depends on parameters a and b c' aspects, and you can also specify and verify global variables access (global_in, global_out).
This with a language that supports tasking, generics, and oop natively...
And proof on access types (pointers) are on the way.
Ada is a positevly amazing language. The only real complaint that can be made about it is the dearth of libraries/non-existent package management and the weird FSF vs. AdaCore compiler licensing issues.
This is a misleading comment, because it oversells Rust and criticises Ada unfairly. Ada and SPARK have a track record of being used to build safety critical systems, unlike Rust.
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.
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.
In one of my job I took a part of creating a compiler for VHDL, which is superset of some old version of Ada (and diverging from it).
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.
39 comments
[ 4.4 ms ] story [ 93.8 ms ] threadRocket 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?
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.
From my understanding, most cubesats do not have propulsion. Can the software render them totally inoperable (other than draining power).
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.
> ... 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.