20. Logic in Programming
Logic in programming studies how formal logic appears inside programming languages, program analysis, verification systems, and tools for constructing correct software. The chapter begins with logic programming, where programs are written as logical rules and computation proceeds by searching for proofs or satisfying assignments. Type systems are then introduced as logical disciplines for classifying programs, ruling out certain errors before execution, and expressing structural properties of data and functions. Verification...