With all the talk about exotic new languages, I just wanted to see if there is any interest out there for an “old”, “boring” language like Ada/SPARK on Genode. (SPARK is an Ada dialect focused on formal verification.)
A few years ago, there was some very interesting work (and Genodians articles) in this area (RIP Spunky ). The work at Genode Labs was discontinued, but I still think there is a lot of potential there.
The concept of memory safety and performance of Ada and Spark is very interesting where it is competing with rust: Should I choose Ada, SPARK, or Rust over C/C++? | The AdaCore Blog . I do not think that much people on here are very much familiar with Ada especially not Spark. A nice approach would be a declarative workspace where Spark can show it’s potential of mathematical proofs to avoid run-time errors.
). The work at Genode Labs was discontinued, but I still think there is a lot of potential there.