logoalt Hacker News

toast0today at 6:37 PM0 repliesview on HN

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification.

Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish.

I do see value in formal verification of IPC/threading communication primitives (locks, semaphores, queues, whatevs), but then formal verification usually require assumptions for hardware behavior and those aren't always correct, so. But I've never used formal methods outside exposure in an undergrad survey class, so I dunno.