Interactive theorem proving (ITP) is a technology for developing and verifying formal proofs, say of software correctness. At present it is laborious to use, but automation and machine learning techniques show promise for improving this situation. This will enable new applications beyond verification. We describe the Formal Abstracts project of Thomas Hales, and the use of ITP to power search engines. We define and discuss ``call by specification'' -- the ability to find and call subroutines by giving a formal specification.