Email the Author
You can use this page to email Sandy Maguire about Certainty by Construction.
About the Book
Agda is not just a programming language; it's a completely new way of thinking about software, and mathematical objects at large. This book is on successfully wielding Agda: teaching everything you need to know to get productive in modeling problems and in verifying your solutions.
Ready for a software revolution?
The software status quo is woefully inadequate when it comes to addressing critical issues. The endless stream of hasty solutions piled on top of earlier slapdash fixes has left us mired in inefficiency. Certainty by Construction boldly proclaims that the solution lies in embracing the elegance of abstract algebra as the cornerstone of software design. Learn to model problems in Agda, and get ready to explore the captivating world of proof assistance.
Discover abstract mathematics
Ever pondered what equality truly means? Intrigued by the prospect of
automatically discovering asymptotic optimizations? Curious about the enigmatic world of monoids and how they birth fascinating programs? Certainty by Construction will unravel these mysteries and guide you on a journey of intellectual discovery.
For veterans and newcomers both
Whether you're a seasoned programmer looking for a new and exhilarating
challenge, or a mathematical amateur eager to embark on an exciting journey, this book is for you. Maguire's engaging approach will empower you to learn Agda and mathematics on your own, and equip you with an arsenal of techniques to break down complex problems into straightforward solutions.
Learn to learn
Discover the invaluable skill of learning mathematics for yourself. Maguire
doesn't just provide answers; he equips you with the tools to become your own mathematician. Don't just read about mathematics—master it for yourself.
About the Author
Sandy might best be described somewhere between independent researcher and voluntarily-unemployed bum. At the ripe old age of 27 he decided to quit his highly-lucrative engineering job and decide to focus more on living than on grinding for the man. It's what you might call a work in progress.
He regularly writes about Haskell and Agda at reasonablypolymorphic.com.