User loginNavigation 
Proofs as programsMany software developers are turned away from verification techniques because providing proofs for algorithms seems something horrible and purely theoretical to them. A newcomer to a proof assistant like Coq or Isabelle needs at least two weeks to be able to prove some simple theorems. And it is difficult to realize that proving has something to do with programming. In order to provide software verification for the masses a different approach is necessary. If one gains more experience with proofs one realizes that writing a proof is not very different from writing a program. Currently I try to exploit the technique of writing a proof like a program. This led to the notion of proof procedures. With proof procedures there is no need to issue proof commands to some proof engine to manipulate the state of the engine. One just writes assertions (i.e. boolean expressions) in a step by step logical manner. A proof look like a procedure. The article Proofs made easy with proof procedures describes the basic approach. By hbrandl at 20120508 17:03  LtU Forum  previous forum topic  next forum topic  other blogs  17108 reads

Browse archivesActive forum topics 
Recent comments
9 hours 54 min ago
10 hours 9 min ago
10 hours 20 min ago
10 hours 54 min ago
11 hours 13 min ago
12 hours 44 min ago
1 day 11 hours ago
1 day 18 hours ago
2 days 4 hours ago
2 days 5 hours ago