The primary objectives in the design of Athena were proof readability and writability. The goal is to allow for structured, high-level proofs expressed in roughly the same style and at the same level of abstraction as the informal proofs that computer scientists and mathematicians write in practice. To that end, Athena uses a Fitch style of natural deduction instead of the more customary sequent systems or proof trees. Fitch-style natural deduction is formalized by means of novel block-structured syntactic constructs and so-called assumption-base semantics.