Answer set programming is a declarative programming paradigm for the development of knowledge intensive applications, especially those that involve combinatorial search. It is rooted in work on the semantics of logic programs, so that syntactically answer set programs are reminiscent of those of Prolog. Yet, the systems that process these programs, and the art of programming in this style, differ from classical Prolog. The process of creating an answer set program involves

1. representing a domain in the language of an answer set solver — a system for processing logic programs,
2. making that representation safe for grounding — a process of eliminating variables of the program by substituting object constants, and
3. tuning the representation to facilitate search efficiency.

The processes involved in making the representation safe and efficient fall into the so-called refactoring, which is a common software engineering practice. In this talk, we will discuss answer set programming and its practices, as well as the proof assistant system called Anthem, which is designed for the purpose of facilitating proofs of correctness of the refactoring process. Examples will be used to illustrate the key concepts of answer set programming the operation of Anthem, and its logical foundations based on the relationship between logic programs under the answer set semantics and the process of converting logic programs into first-order logic formulas called completion.