Why can’t programs be proven?

Proofs are programs.

Formal verification of programs is a huge research area. (See, for example, the group at Carnegie Mellon.)

Many complex programs have been verified; for example, see this kernel written in Haskell (repaired 404 link is for seL4, see also the moved to location and the project’s website).

Leave a Comment