Is there any production software in the world that is written and maintained in a formally verified language? I have only ever seen toy problems and simplified subsystems of real projects verified.
I work on space craft flight software and exactly none of it is formally verified. As far as I know, it's not practical to do so. If we could do it (without ballooning cost and schedule 10x), we would.
I work on space craft flight software and exactly none of it is formally verified. As far as I know, it's not practical to do so. If we could do it (without ballooning cost and schedule 10x), we would.