Over 40 years ago, Bob Constable and his students started designing a logical language for specifying programming tasks and mathematical problems. The system, called Nuprl, is known since 1984 for being able to synthesize correct-by-construction programs from formal proofs in constructive type theory.

The Nuprl Library holds over 15,000 mathematical theorems, with a database of 450,000 proof steps, dealing with pure mathematics as well as proofs of programs. Bob received the 2014 Herbrand Award for this pioneering research in automated reasoning.

Bob was also the leading force in Cornell’s creation of CIS ---the Faculty of Computing and Information Science ---which has helped bring computing and computer science into every Cornell college. Bob served as first dean of CIS for ten years.

Bob and interviewer David Gries talk about the old days in CS.

Running Time: 47 min. http://hdl.handle.net/1813/40560