While much of today's AI focuses on statistical methods, a well-established parallel exists in the form of symbolic, also known as Good Old-Fashioned AI (GOFAI). Here, programs manipulate logical formulas to solve strictly defined problems through reasoning rather than learning. Automated theorem provers, for example, search for formal proofs and refutations by applying logical rules. However, writing such algorithms is tricky. How can we guarantee that they follow those rules correctly? More importantly, how can we be certain that they terminate and provide an answer? This talk explores how to build autoproving algorithms that are guaranteed to halt using a functional domain-specific language of combinators in Agda. The key insight is to use a well-behaved class of recursion: we design our algorithms so the type system can verify that they always make progress toward a solution. We examine how classical algorithms such as resolution and unification can be expressed within this framework, where our combinators handle the complex proofs behind the scenes while we focus on algorithm logic. This creates a curious circularity, as type-based reasoning itself relies on such methods. Whether you're interested in symbolic AI approaches, automated reasoning systems, or advanced type systems, or are working on systems where correctness guarantees matter, this talk shows how functional programming techniques can make software both more reliable and more concise while demonstrating the capabilities of dependent types in action.