User loginNavigation 
archivesProofs 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. Reducers  A Library and Model for Collection ProcessingRich Hickey's post on Reducers  A Library and Model for Collection Processing By adopting an alternative view of collections as reducible, rather than seqable things, we can get a complementary set of fundamental operations that tradeoff laziness for parallelism, while retaining the same highlevel, functional programming model. Because the two models retain the same shape, we can easily choose whichever is appropriate for the task at hand. 
Browse archivesActive forum topics
New forum topics

Recent comments
4 hours 22 min ago
8 hours 41 min ago
10 hours 29 min ago
11 hours 49 min ago
14 hours 33 min ago
16 hours 18 min ago
16 hours 43 min ago
16 hours 45 min ago
18 hours 38 min ago
20 hours 56 min ago