Who is this important for? Is there a lot of software still being developed for POWER? It seems niche to me, but maybe I'm the one in a niche.
In my opinion, an area of interest going forward into the next decade of more safety-critical software written by smaller and smaller orgs (e.g. eVTOL companies, sensor companies, etc) is continuing to push forward which objectives can be accomplished by formal means instead of primarily through testing.
An NXP or IBM processor might be great, and might be mature, and might be very well tested -- but I, as a safety-critical software developer, have little way of demonstrating that to certification authorities. The availability of open-source processor designs and, in the future, traceable and accountable conversion from those HDL designs to RTL, to masks, and then to silicon, gives a path to showing that portions of a processor are correct-by-design, and thus a path to the goal of showing that my machine-code-as-authored(-by-an-assembler) and machine-code-as-executed(-by-a-processor) semantics match.
Any process can be used well or poorly, and DO-178C isn't really a process, it's a set of objectives that a process must accomplish. When used in good faith, I believe it can lead to software of higher quality than almost any other approach (although, to be fair, at higher software development cost than almost any other approach). That doesn't mean that chanting the document name and using hand-me-down rituals is sufficient to achieve high quality software, of course :-).
and in the Mars Rover, which is a radiation-hardened 133mhz 32-bit Power ISA system.
The Talos is currently the only fully libre computer available for high-perf computing, and it uses POWER9 CPUs. If you want a fully free CPU, your choices are either very dated CPUs or POWER.
Many distros (inc. Debian, and most source-based ones) support ppc64/POWER officially quite well and go out of their way to ensure a high degree of portability.
Yes, you can just install most of at least Debian, Fedora, RHEL, at least, though it needs an "alt" kernel on RHEL7 P9. There are a few things which haven't been ported, mainly due to assembler, I guess. (PRoot and DMTCP are two I know.) Even x86 SIMD intrinsics will largely work, if not necessarily very efficiently.
The fact that the POWER architecture may be niche is not a problem since so much software can be compiled for it. See the thalos workstations: https://www.raptorcs.com/TALOSII/ and the powerpc notebook: https://www.powerpc-notebook.org/en/
For people who are willing to use niche hardware for more control on what is running, this is seems like a very important step.
What's good about this is that the source is available and can be verified to some degree against the hardware (by decapping it.) That puts a log of constraints on what kinds of secret back doors people can build that we didn't have before.
before you even get to that stage, you run the Formal Correctness Proofs and unit tests on the HDL, so that YOU have confidence that the HDL which you're about to generate the GDS-II files from is actually correct and does the damn job.
example of a Formal Correctness Proof for the fixed arithmetic Power ISA pipeline:
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu...
runs with symbiyosys, so you end up running SAT Solvers like yices2 and z3.
basically we absolutely do not want to be the people you come to and say, "can we trust your ASIC?" and like Intel they lie to you and say "of course!", we want to say, "don't bloody well ask us, go run the damn tools yourself! oh, btw, if you want help with that we charge USD 5k per hour"
https://git.libre-soc.org/?p=power-instruction-analyzer.git;...