> 'Click to write and install driver’

Theo de Raadt would spin in his grave — after the security implications of this to OpenBSD gives him a fatal aneurysm.

Either that, or he'll surprise-launch OpenLLM, a model bundled in the next OpenBSD release that produces driver code free of security bugs.

▲

sterlind 3 hours ago | parent | next [-]

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.

	▲	speed_spread 2 hours ago \| parent [-]
		That's also assuming the device is fully documented and that hardware behaves exactly as documented.

▲

ktta 3 hours ago | parent | prev [-]

> Theo de Raadt would spin in his grave

Isn't he still alive?

	▲	boomlinde 3 hours ago \| parent [-]
		> — after the security implications of this to OpenBSD gives him a fatal aneurysm.