eggy

Don't forget this list of expectations for SPARK [1] too, if you want even safer, high-integrity, and formally verified code on Android!

[1] https://www.adacore.com/about-spark

I've heard this one before. I still use Mathematica (Home edition). It has curated data and more than just a notebook interface, which it pretty much invented. I use Julia with Pluto, SMath Studio, Frink, and some others for Maths toolbox. I love to play in Mathematica. It is function rich and the documentation is amazing. I usually prototype/research in it. But then again, I drop to BQN/APL/J for some math fun.

There's more than just memory safety for high assurance apps. Personally, I think Rust is heading in the right direction, but I am not sure it's complexity will ever be smooth or enjoyable for some. I feel you get most, if not all, that Rust is trying to achieve with Ada/SPARK right now for high-integrity, mission-critical apps along with a proven legacy: jet fighter software, railway controls, avionics, embedded, space, etc...

Take a look at the Adacore site, especially the free books (PDF):

https://www.adacore.com/books

Ada for the Embedded C Developer

Embedded Spark & Ada Use Cases

Enjoyment is part objective and a lot subjective. Mitchell Hashimoto who wrote Ghostty in Zig speaks about it here: https://youtu.be/YQnz7L6x068?si=VtH2FEAuW-SiFPHr&t=1415

I started with 6502 assembly and PET Basic in 1977, so for me, Zig is simpler, and jives more with me than Rust. OTOH, I chose Ada/SPARK for our product for the high-integrity, mission-critical aspect of our automation software. I programmed in Pascal back in 1988, and it has the same syntax, which I always found verbose and boring, but it is clear and structured and the concepts to achieve this level of high assurance are not too difficult. For ultiimate fun, I program in J/APL and now mainly BQN, so I am not a fan of verbosity!

I would have been more attracted to Rust if it had kept ML-like syntax from OCaml and not the Algol-like curly braces of C/C++.

Adacore is doing great work. They have a Rust compiler, but the static analysis and formal verification is not quite there for the Rust toolchain and it does not have any where near the legacy for high-integrity, mission-critical apps. Not that it is not heading that way, but for us it is not there by a longshot to select it for our product.

In performing an assessment of which ecosystem and PL to use to develop our high-integrity automation software for mission-critical applications, we assessed Rust, Zig, and Ada/SPARK. Rust had the support behind it from a big corp., a passionate developer community, and some adoption by significant entities, but none with cyber-physical systems. And it has been interesting to see some developers leaving Rust for Zig for the sheer enjoyment of using it instead. Our software will be controlling machinery overhead and other close coupling with machinery and people. Rust does not have the legacy in these areas or the ecosystem to cover formal verification. Zig was considered, but was even more new than Rust, and had similar disadvantages as listed for Rust. SPARK, a relatively newer PL, a subset of Ada, has legacy in high-integrity, mission-critical applications, and formal verification tooling that along with human review, makes it the strongest choice to meet the government's latest push for such critical software, and the language though verbose, is low friction to learn and apply. I found Zig to be a great second choice, and look forward to both Rust and Zig's future. Glad to see Zig moving along since Andrew started it. Congrats Andrew and the team currently pulling this off!

Reasons to use SPARK for embedded instead of Rust.

>"According to sources familiar with the huge data transfer outside of the EU country, it occurred in early August. Intelligence sources said Unit 8200 planned to transfer the data to the Amazon Web Services cloud platform. Neither the Israel Defense Forces (IDF) nor Amazon responded to a request for comment."

So was the data moved in August to Amazon (AWS)? I am sure the $3.8bn USD the US gives annually will pay for it anyway. Because it is given as a loan, no accountability is required if it were a grant to Israel, and then the US forgives the loan, so there's not payback or interest for borrowing.

Looks great, I'll have to play with it this weekend! Has a scent of Orca

https://github.com/hundredrabbits/orca

I never did that! Beats typing it in, but then again, I memorized the formula for creating a planar view of the 4 major moons of Jupiter at a given time by programming it all in PET Basic!

I had my Commodore PET for 10 years from 1977 to 1987 until I went away and my cousin borrowed it, and then believing I was not coming back to the US from Spain, sold it!

I loved the cassette drive and all-in-one chassis. Ah, typing in programs from magazines and creating programs from scratch with PET graphics on the keys! I miss those days. So much wonder and fun.

I've always liked generative art and I am getting up to speed on Ada 2022, so this is a fitting article. Currently using SPARK2014/Ada 2022 for a high-integrity, safety-critical automation control software project.

When I started to really get into robotics, mechanics, and automation back in the late 80s and early 90s, the fork in the road of Rodney Brooke's subsumption architecture, but still digital, approach versus Mark Tilden's BEAM analog approach really had me trying both.

CPGs (Central Pattern Generators) were often implemented using simple RC (resistor-capacitor) circuits within his "nervous net" (NvNet) architectures. The RC circuits generated rhythmic patterns that drove the robots' motor behaviors, allowing gaits to emerge naturally from the interaction of these analog components with the environment and the robot's mechanical structure. This approach enabled adaptive, robust locomotion without requiring complex digital control systems.

His 6-legged robots could lose a leg, and the system would take feedback from the stuck or missing leg, and learn to walk with 5 or 4 legs. Amazing stuff.

Yes, but a qualified compiler is but one of many pieces in having an ecosystem/tooling for creating, testing, and having high-integrity applications reviewed and certified. A couple of the industries we are elbowing in on, are already familiar with the type of reports generated by the AdaCore tooling. Ada has a decades-long history in safety-critical systems (e.g., Boeing, Airbus, NASA), with proven reliability in real-time, embedded applications.

AdaCore’s GNAT Pro suite includes qualified tools (e.g., GNAT Pro, CodePeer, GNATcheck) that support traceability, code coverage, and certification evidence for standards like MISRA, DO-178C, and EN 50128. These are battle-tested in aerospace, defense, and medical applications.

Ada is defined by an ISO standard, specifically ISO/IEC 8652. The latest revision, as of 2025, is Ada 2022 (ISO/IEC 8652:2023), which includes updates to the language features. Ada is also recognized as an ANSI standard through its adoption by the American National Standards Institute, aligning with the ISO specification. The standard defines the language’s syntax, semantics, and features, ensuring consistency across implementations including compilers.

Rust’s safety guarantees prevent many runtime errors, but its approach relies more on programmer discipline vs. Ada/SPARK2014's "correct by construction" methodology. Ada is designed for real-time systems, with built-in features like tasking, protected objects, and precise control over timing (e.g., Ravenscar profile), optimized for cyber-physical systems.

Excuse my verbosity, but I pulled a few things from our tech pitch deck, and a little of the above is in our business plan as well that I copy/pasted.

Two great books if you're interested:

Analysable Real-Time Systems: Programmed in Ada (2016)

Building High Integrity Applications with SPARK (2015)

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.

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.

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.

For my safety-critical automation software for a machine that will operate around people and overhead, I’m choosing Ada/SPARK2014. Its decades-long track record in high-integrity domains like aerospace, defense, and medical systems ensures reliability for applications where human safety is paramount. SPARK2014’s formal verification tools mathematically prove the absence of runtime errors, aligning with standards like DO-178C and ISO 26262, critical for my Q3 2026 market deadline. While Rust is gaining traction for memory safety, its formal verification tools, like LEAN/Aeneas, are still maturing and lack the production-ready ecosystem of Ada/SPARK2014. Ada’s clear, structured syntax simplifies code reviews, and its tooling generates certification reports familiar to regulators, streamlining approval processes. For my project’s safety and business needs, Ada/SPARK2014 is the proven choice - for now. I am not a fan of Rust syntax or complexity, but that is somewhat subjective. I last dove in about 2 years ago.

Did you account for the paper band that wraps the 100 one-dollar bills? Not nitpicking, but you said you counted everything you could see.

It should be between 0.002-0.004 in. thick, so each band per bundle is about 0.004 to 0.008 thick. Might take off a little bit of your overage.

Great article!

The excitement kind of ebbed early on with seeing the video and realizing it had a plate/weight on one face.

"A few years later, the duo answered their own question, showing that this uniform monostable tetrahedron wasn’t possible. But what if you were allowed to distribute its weight unevenly?"

But the article progressed and mentioned John Conway, I was back!

Great example, and telling of all the uses, mushrooms, and their ilk are being praised and touted as beneficial

Article is three years old, and the fungi are not talking to us! I imagine the communication being a bit slow like the scene in the kids animated movie, Zootopia, where sloths work at the DMV..."P....L....E....A....S....E-------" don't tread on me! However, if like German 1 word can cover a whole concept, then 50 words may be sufficient to communicate in a reasonable time scale ;)

I spent 6 months in Saudi in 2022 and 2 months in 2023, and I went to the UAE and did business with both countries. They've been on this wave like the world has. The UAE mandated AI education in their schools, are acquiring and training talent, and have huge, huge amounts of money invested in developing on all fronts from education to engineering to application for their 2031 initiative. The AI genie is out of the bottle, and although OpenAI is a hybrid non-profit / for-profit company in that they have for-profit LLCs that are managed by the non-profit, so this gets murky. See OpenAI Holdings, LLC and OpenAI Global, LLC. I don't think you can monopolize technology such as AI when computing hardware is expanding in capability and cost is going down as well as the immediate ability to read research papers, YouTube videos, books, and all media available on the internet or other media venues. The Saudi Digital Library in the largest digital library in the Arab world. Is China's AI better than the West's? They've certaily implemented a lot of real world installations and applications of it, but I am not sure how it compares to the NSA pre and post Snowden.

The less than 400k population is a good sample size, however, their main revenue comes from tourism, aluminum smelting, and fisheries, and they have a relatively large source of geothermal and hydropower with a very homogenous population (>80% Icelandic). Data centers are about 1% of its GDP. Even Iceland needs barkeeps and restaurant workers to work at least 5 days/week with restaurants in touristy areas open 7 days/week with shorter days on Sunday. Having worked a life of manual labor and white-collar jobs, sometimes both in the same job, the 4-day work week is really for specific types of industry or work. Tech, for sure, but not the food service industry...

Glad you found it. I've done much worse, believe me!

If you have any questions check out the Google Groups (no Groups comments!) for Shen. I am eager to see the 5th edition, and I will probably buy the print version.

Other than the online version (4th edition), I don't know of any other place to get it. Yes, the paperback was expensive, but I bought it anyway. It proved to be very informative and more substantive than I had thought. I believe the 5th edition is almost ready for publication.

You're right: Shen's mathematical underpinnings (sequent calculus, dependent type theory) can intimidate programmers without a formal logic background. I bought the "The Book of Shen" (TBOS) revision 1 and revision 3. Revision 4 is available on the website. It's a great book with some CS history, logic, and development of Shen from Qi as well as how everything works in Shen including the type system.

Shen uses a dependently typed Sequent-Calculus based Type System (SCTS). It uses type rules vs. type classes, and type checking is optional, you can turn it on or off. Haskell's type inference makes things a bit simpler, and is a battle-tested static type system with excellent type inference which lends itself better for functional programming and large-scale software engineering (for the moment). Shen's TC is more expressive, but requires more effort.

Aditya Siram has some old but goody YT videos on Shen.

It's resolved. I helped support it for a brief time for the SP version, which is now integrated into the latest version. You're right though, that this put many people off.

You should check out Shen[1]. It is a portable functional programming language. Optional type checking and it solves my affair with Lisp and Haskell. It is a Lisp.

[1] https://shenlanguage.org/

Nice! I have been toying with KolibriOS and MenuetOS for my anti-social platform. You can network on both, and sometimes requires a direct hardwired Ethernet cable. Originally I was interested in them given they are written in assembly using FASM. I was a 1977 CBM (Commodore PET 2001), so I am more of a lime-green on black screen vs. the DOS grey/blue. Cool!