honestly LLMs could probably write drivers in CompCert C or some other formally verified dialect. having AI discharge proof obligations seems like a terrific use for all this newly-developed mathematical process.
replyyou could have the driver code prove it implements a spec, that there's no UB, that hardware invariants are maintained, that routines take a fixed time to execute.
the formal driver spec must still be written by sober, well-caffeinated humans of course.
That's also assuming the device is fully documented and that hardware behaves exactly as documented.
replyAnyone who has done any work with hardware can confirm that neither of these things is ever true. :(
reply> Theo de Raadt would spin in his grave
replyIsn't he still alive?
> — after the security implications of this to OpenBSD gives him a fatal aneurysm.
reply