top | item 45862853

(no title)

OK can someone smarter than me educate me?

A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad.

At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code.

I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6...

I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).

discuss

AlotOfReading|3 months ago

There's a lot to unpack here. You can always make a stricter programming language by having your compiler error on everything.

Lisps are perfectly usable for system level code as well. There was an entire lineage of Lisp Machines where virtually all OS code was written in lisp. Those probably could have used ACL2 had it existed.

There's an X-Y component to your questions though. The strictness of the programming language just isn't the main goal for OS formal verification. It just makes certain things easier. What's important is having executable semantics of the programming language, having a machine model, and a behavioral specification. All of these are typically written in proof languages, and the kernel code is proven to implement the behavior spec according to the machine and language semantics.

SPARK gives you executable semantics, but so do C (specifically the Clight subset), most of the Lisps, Rust, and many others. You're benefiting from certain errors being impossible in SPARK, but it's not a fundamentally different process.