Reasons why you don't prove your programs are correct - comp.software-eng

Message from discussion Reasons why you don't prove your programs are correct

Dave Decot

More options Jan 18 1990, 4:30 pm

Newsgroups: comp.software-eng

From: de...@hpisod2.HP.COM (Dave Decot)

Date: 18 Jan 90 21:30:11 GMT

Local: Thurs, Jan 18 1990 4:30 pm

Subject: Re: Reasons why you don't prove your programs are correct

  Reply to author
  |
  Forward
  | Print
  | View thread
  | Show original
  | Report this message
  | Find messages by this author
  

Here's three of my reasons why programs aren't proved correct.
(Sorry I was unable to reach you by email.)

Theorem provers are too slow and expensive.

Programmers are too lazy to write assertions and invariants, especially
for complex code (which if they weren't lazy wouldn't be so complex).

Efficient compilers for programming languages that support automatic
verification are not widely available.

Dave

Reply to author Forward