Yep we have come a long way from Slackware 2.0. How times change.
I have been following Azure Sphere since the early days, but what I still miss from all available documentation and presentations, is what Microsoft is doing at C level for a platform whose selling point is security.
I would expect them to take this opportunity to push Checked C, or hardware pointer tagging (like on SPARC) into mainstream.
So it is not impossible Azure Sphere would explore it.
The problem is all that is nice and cool, but the real world IoT is about Chinese cams by Dahua of MIRAI fame and ESP32 modules with barely working WPA. Because the price is low, and that's what matters at scale.
What if perfectly secure, formally proved and verified code would be simultaneously the cheapest to produce, considering developers time, code performance and other business metrics? What if the guy in Shenzhen would download not the bunch of C libraries from Github and hack it until it don't crash for at least 5 minutes on the new version of the SoC, but download instead a Coq code, proved by best and brightest Stanford researchers, and just tweak the hardware spec a little - then generate the fastest possible assembly code from it, with test, quick and automagically? What if another guy in Shenzhen, who need to hack a bunch of IPs to build that SoC as fast as possible, and tape it out before other guys, would do the same to generate the RTL - not because it's cool or right, or anything - but because it's faster and cheaper than hacking Verilog and write all the test scripts to verify the SoC don't hang up too often.
Maybe we need a dozen of projects like https://deepspec.org for make it happen, but I think there's no another way to really change the state of affairs.
Back in the day, I remember running SLS Linux[1] on a 4MB PC and that included X11. Of course, a 4MB swap partition on my 40MB drive was a requirement.