Comment by sterlind
11 hours ago
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.
you 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.
Anyone who has done any work with hardware can confirm that neither of these things is ever true. :(