This talk studies how slicing can remove redundancy from programs and proofs. In the first part, we introduce type-directed program slicing, which uses typing rules to build declaration dependencies, slices from a target, and employs the compiler as a dynamic oracle to further minimise the program while preserving well-typedness. In the second part, we examine whether this idea can be transferred to proof assistants.