> Yes I know Ada is not a good fit, but there has already been a Unix-like OS entirely implemented in a derivative of Pascal: TUNIS.
Isn't it? There is a very well-developed kernel written in ADA with SPARK and formally verified at that: https://ironclad.nongnu.org
And PASCAL-derived languages were very popular for operating systems in the 80s. To name a few: Apple's LISA OS, DEC's VAXELN, and OBERON. There were others as well that didn't quite make it, like DEC's MICA and Acorn's ARX.
Isn't it? There is a very well-developed kernel written in ADA with SPARK and formally verified at that: https://ironclad.nongnu.org
And PASCAL-derived languages were very popular for operating systems in the 80s. To name a few: Apple's LISA OS, DEC's VAXELN, and OBERON. There were others as well that didn't quite make it, like DEC's MICA and Acorn's ARX.