"It would be very interesting if somebody could write formally verified small, trusted part of these projects. It would be interesting if somebody could write formally verified pledge kernel's subsystem. "
I agree, but I am open to being wrong.
I think if OpenBSD dev community managed to write some small part of OpenBSD in a mathematically proven way, they would learn something while doing it, that would in the long therm improve code quality of the rest of the project as well.
Because the development infrastructure regarding compilers/programming languages probably would need to be improved in order to do such task. C is only practically possible to prove in very small code, from my understanding after googling.
|