there have been attempts at writing kernels using stuff like Coq https://www.cs.columbia.edu/~rgu/publications/cacm19-gu.pdf
I got Asahi working on M1, and everything works fine aside from the camera and hibernation. The second is a bit of a bummer cause the battery keeps draining fairly quickly even when you put it to sleep.
O7
take a look at Apache Ignite https://ignite.apache.org/docs/latest/tools/sqlline
there’s also datafusion that lets you run SQL commands via CIL on CSV and JSON https://datafusion.apache.org/user-guide/cli/usage.html
I’ve been running my own nextcloud for around a decade now. I use it for my calendar, contacts, and file storage. It’s basically replaced all the google services for me, and has been effectively zero maintenance. It just works.
I really like fish because it has excellent contextual autocomplete based on the folder you’re in. I haven’t used any other shell that was as good at it.
Linux and open source in general completely blow apart capitalist arguments that profit motive is necessary for innovation and technological advancement. Open source ecosystem primarily run by volunteers has produces some of the most interesting and innovative technologies that we’ve seen. The reality is that people make interesting things because they’re curious and they enjoy making stuff. Pretty much nobody makes anything interesting with profit being the primary motive.
You’r right that only OCaml and Haskell can be used as extraction target for Coq programs. However, it is possible to use Coq to write verified C software. On example is the Verified Software Toolchain that lets you translate C programs to a format that Coq understands and can prove theorems regarding their behavior.