I always enjoy stories about Ada, Pascal, Object Pascal, Prolog, Perl, OCaml, Standard ML, Forth, Pike, Fortran, Scheme, Common Lisp, or some APL derivative in use in the wild.

It’s especially good to see a story about a recent project on a smaller system using Ada.

At a lower level in the formal verification stack than this, it's on the one hand awesome that ARM has published a machine readable architecture specification for the more recent A architectures in ASL... and on the other hand extremely frustrating that they haven't done the same for M.

I'll read more later but just keep in mind nucleo is a series of form factors. There's even M33 on a -144 which is ARMv8-M