Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

gautiersblog.blogspot.com

Post reply on HN
Print view View original

61–70 of 72 posts

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#61

Post by carlmr »

tombert wrote: post #27
imglorp wrote: post #17

Earlier quoted context omitted.

Failed what? In its domain, it succeeded in its goals: a high reliability platform for aerospace, defense, and other mission critical domains. It was mandated by the US DoD for all software in the nineties and used in Airbus avionics and aboard the ISS, etc. Its syntax and concepts were considered solid and so was selected as the basis of the VHDL hardware description language, also successful in its domain.

Failed in the sense that it doesn't appear to be used anymore. C and C++ are still used pretty frequently. I wouldn't say that they failed, but if someone wrote an application in Ada in 2025, I would find that a bit anachronistic.

Anachronistic maybe, but it would still make a lot of embedded development a whole lot easier to get right. Modern Ada has a much better set of features compared to C, doesn't have the bloat of C++, and allows much better handling of embedded issues like fixed point calculations than either of them.

It's still a very modern language which is missing very little in that niche. It's only missing adoption.

I have high hopes for Rust in this space. Using C is fine, using C++ is madness, using Ada is good but fewer available devs.

Rust also solves a lot of issues with C++ and generally, once you get past the "fighting the borrow checker" to the "working with the borrow checker" phase has insanely good ergonomica, safety mechanisms and features. Additionally Rust has momentum right now.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#62

Post by cashsterling »

I think Ada is a great language and it is completely possible that Ada will experience a resurgence in coming years.. especially as LLM's are used more and more to generate software. ADA/Spark can provide very robust guide rails for correctness (so can Rust) of 'AI' generated code.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#64

Post by etrez »

whartung wrote: post #6

Well that was disappointing. I was hoping to see a discussion about writing a zip encoder in Ada. How the language was used, values of the language for this kind of work. How it’s easier or harder to do. Maybe a bunch of Ada source code. Simply as one who does not use Ada I had hoped to be a bit more informed about it.

Thanks for the feedback. Multiple posts are planned on that topic. For parts 1 and 2 (so far the only ones existing) I preferred explaining the context and the remarkable simplicity of the BZip2 format. In part #4, I will try to show why the customisable types in Ada fit so well compression software. Be patient: writing articles about writing software takes much more time than writing the software itself! In the meantime, there is a short preview of that in recent presentations - notably FOSDEM 2025: https://fosdem.org/2025/schedule/event/fosdem-2025-5148-adve... , last slide.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#65

Post by MaxBarraclough »

steveklabnik wrote: post #38
MaxBarraclough wrote: post #32

Earlier quoted context omitted.

Doesn't Rust lack a serious language specification? How can compilers be certified without a definitive record of how the language is meant to behave?

A language specification is not required to be qualified. The behavior of the compiler needs to be described. https://rust-lang.github.io/fls/ This is effectively a fork of the Rust Reference, made by Ferrous, and laid out in a way that allowed the compiler to be qualified. It now lives at this URL, because it's being adopted by upstream as the spec.

Sounds like progress is being made on the language spec front, that's good to see.

I'm not following what you meant by this though, it seems like a contradiction:

> A language specification is not required to be qualified. The behavior of the compiler needs to be described.

But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described.

Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language?

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#66

Post by steveklabnik »

MaxBarraclough wrote: post #65
steveklabnik wrote: post #38

Earlier quoted context omitted.

A language specification is not required to be qualified. The behavior of the compiler needs to be described. https://rust-lang.github.io/fls/ This is effectively a fork of the Rust Reference, made by Ferrous, and laid out in a way that allowed the compiler to be qualified. It now lives at this URL, because it's being adopted by upstream as the spec.

Sounds like progress is being made on the language spec front, that's good to see. I'm not following what you meant by this though, it seems like a contradiction: > A language specification is not required to be qualified. The behavior of the compiler needs to be described. But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surel…

> to enable certification

It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases.

You’re always going to need to have more than a language spec because you qualify compilers not languages.

> Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described.

It has. At least to the degree that regulators find it acceptable.

> Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language?

There is no difference in flavors, but it is true that each version of the spec is for a specific version of the compiler, and so sometimes that will lag a bit. But that’s just how this process works.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#67

Post by MaxBarraclough »

steveklabnik wrote: post #66
MaxBarraclough wrote: post #65

Earlier quoted context omitted.

Sounds like progress is being made on the language spec front, that's good to see. I'm not following what you meant by this though, it seems like a contradiction: > A language specification is not required to be qualified. The behavior of the compiler needs to be described. But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surel…

> to enable certification It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases. You’re always going to need to have more than a language spec because you qualify compilers not languages. > Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. It has. At le…

Thanks for the reply. Interesting developments for the language.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#68

Post by eggy »

steveklabnik wrote: post #66
MaxBarraclough wrote: post #65

Earlier quoted context omitted.

Sounds like progress is being made on the language spec front, that's good to see. I'm not following what you meant by this though, it seems like a contradiction: > A language specification is not required to be qualified. The behavior of the compiler needs to be described. But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surel…

> to enable certification It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases. You’re always going to need to have more than a language spec because you qualify compilers not languages. > Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. It has. At le…

I considered two things when choosing SPARK2014 over Rust: field-proven legacy apps and a language spec tied to the tooling AND the compiler.

A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#69

Post by steveklabnik »

eggy wrote: post #68
steveklabnik wrote: post #66

Earlier quoted context omitted.

> to enable certification It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases. You’re always going to need to have more than a language spec because you qualify compilers not languages. > Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. It has. At le…

I considered two things when choosing SPARK2014 over Rust: field-proven legacy apps and a language spec tied to the tooling AND the compiler. A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec.

> A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec.

I don’t understand. That’s a requirement for qualification.

Re: Writing a competitive BZip2 encoder in Ada from scratch in a few days (2024)

#70

Post by eggy »

steveklabnik wrote: post #52
eggy wrote: post #51

Earlier quoted context omitted.

That's for automotive. We're shooting for a bunch of various relevant standards. There is no formal language spec. Who did that compiler? AdaCore's been around for a long time, so I am quick to use theirs if I were to chose Rust. I'm also following the Ironclad kernel project with its complementary OS called Gloire. Ada/SPARK for both with partial formal verification progress.

Automotive is the first industry that’s really taking up Ferrocene! They’re adding more stuff as more industries have demand for it. Ferrous and AdaCore were originally collaborating, but then they parted ways. In my understanding they’re both largely the upstream codebase, I know that the Ferrous folks religiously upstream almost everything, no clue if AdaCore does as well.

I am excited Rust is heading in this direction. We had to go with SPARK2014/Ada (2022) when we made this decision over a year ago. Rust and its tooling was and is not ready for the safety critical control system we are developing. High-integrity, safety-critical auditors in government and industry are already aware of the types of reports generated by the AdaCore tooling, so this makes less friction in seeking these certifications. We are also hoping the Ironclad Kernel and Gloire OS gain traction. A kernel written in SPARK2014 and fully formally verified and a complementary OS using Ironclad would make it turtles all the way down to our bare metal controller up to the control system application and HMI. I will certainly keep Rust on my radar in the future. Do you have any examples of where Rust is mainly the PL used in a CPS (Cyber-Physical System) that requires this level of integrity and safety? SPARK has applications in avionics and other industries that go back for decades: Typhoon EuroFighter - flight control and mission-critical systems; Harrier GR9 - avionics; UK NATS iFACTS System - safety-critical air traffic control software; LifeFlow Ventricular Assist Device - medical device to support heart function. SPARK was used for its control software, and the list goes on and on.
Post reply on HN