Comment

Comment by nl

I'm not sure you are aware, but formal verification[1] is a well known and respected field of research. It does work, but it is hard to build practical tools using it. Nevertheless, if something is formally proven correct then for it to be incorrect one of three things must happen:

1) The proof is incorrect (which of course means it is no longer proven)

2) The prover has a bug (most proofs are done automatically). This is possible, but many of the same formal methods are used on the prover, and it is often build on a human-proved proof at the bottom.

3) Mathematics (the whole field) is wrong. This seems unlikely.

In reality, the problem with formally verified software is generally that it must interact with non-verified software (and sometimes hardware - although hardware can be verified too).

The wikipedia page[1] I referenced is worth reading.

[1] http://en.wikipedia.org/wiki/Formal_methods

parent nl 12 years ago

Discussion

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton