Certainty by Construction
Minimum price
Suggested price

Certainty by Construction

Software and Mathematics in Agda

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.

  • Share this book

  • Categories

    • Functional Programming
    • Mathematics
    • Computer Science
  • Feedback

    Email the Author(s)

About the Author

Sandy Maguire
Sandy Maguire

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.

Table of Contents

  • Contents
  • Preface
  • The Co-blub Paradox
  • A Gentle Introduction to Agda
    • The Longevity of Knowledge
    • Modules and Imports
    • A Note on Interaction
    • Importing Code
    • Semantic Highlighting
    • Types and Values
    • Your First Function
    • Normalization
    • Unit Testing
    • Dealing with Unicode
    • Expressions and Functions
    • Operators
    • Agda’s Computational Model
    • Stuckness
    • Records and Tuples
    • Copatterns and Constructors
    • Fixities
    • Coproduct Types
    • Function Types
    • The Curry/Uncurry Isomorphism
    • Implicit Arguments
    • Wrapping Up
  • An Exploration of Numbers
    • Natural Numbers
    • Brief Notes on Data and Record Types
    • Playing with Naturals
    • Induction
    • Two Notions of Evenness
    • Constructing Evidence
    • Addition
    • Termination Checking
    • Multiplication and Exponentiation
    • Semi-subtraction
    • Inconvenient Integers
    • Difference Integers
    • Unique Integer Representations
    • Pattern Synonyms
    • Integer Addition
    • Wrapping Up
  • Proof Objects
    • Constructivism
    • Statements are Types; Programs are Proofs
    • Hard to Prove or Simply False?
    • The Equality Type
    • Congruence
    • Identity and Zero Elements
    • Symmetry and Involutivity
    • Transitivity
    • Mixfix Parsing
    • Equational Reasoning
    • Ergonomics, Associativity and Commutativity
    • Exercises in Proof
    • Wrapping Up
  • Relations
    • Universe Levels
    • Dependent Pairs
    • Heterogeneous Binary Relations
    • The Relationship Between Functions and Relations
    • Homogeneous Relations
    • Standard Properties of Relations
    • Attempting to Order the Naturals
    • Substitution
    • Unification
    • Overconstrained by Dot Patterns
    • Ordering the Natural Numbers
    • Preorders
    • Preorder Reasoning
    • Reasoning over ≤
    • Graph Reachability
    • Free Preorders in the Wild
    • Antisymmetry
    • Equivalence Relations and Posets
    • Strictly Less Than
    • Wrapping Up
  • Modular Arithmetic
    • Instance Arguments
    • The Ring of Natural Numbers Modulo N
    • Deriving Transitivity
    • Congruence of Addition
    • Congruence of Multiplication
    • Automating Proofs
    • Wrapping Up
  • Decidability
    • Negation
    • Bottom
    • Inequality
    • Negation Considered as a Callback
    • Intransitivity of Inequality
    • No Monus Left-Identity Exists
    • Decidability
    • Transforming Decisions
    • Binary Trees
    • Proving Things about Binary Trees
    • Decidability of Tree Membership
    • The All Predicate
    • Binary Search Trees
    • Trichotomy
    • Insertion into BSTs
    • Intrinsic vs Extrinsic Proofs
    • An Intrinsic BST
    • Wrapping Up
  • Monoids and Setoids
    • Structured Sets
    • Monoids
    • Examples of Monoids
    • Monoids as Queries
    • More Monoids
    • Monoidal Origami
    • Composition of Monoids
    • Function Extensionality
    • Setoid Hell
    • Function Extensionality
    • The Pointwise Monoid
    • Monoid Homomorphisms
    • Finding Equivalent Computations
    • Wrapping Up
  • Isomorphisms
    • Finite Numbers
    • Vectors and Finite Bounds
    • Characteristic Functions
    • Isomorphisms
    • Equivalence on Isomorphisms
    • Finite Types
    • Algebraic Data Types
    • The Algebra of Algebraic Data Types
    • Monoids on Types
    • Functions as Exponents
    • Wrapping Up
  • Program Optimization
    • Why Can This Be Done?
    • Shaping the Cache
    • Building the Tries
    • Memoizing Functions
    • Inspecting Memoized Tries
    • Updating the Trie
    • Wrapping It All Up
  • Appendix: Ring Solving
    • Rings
    • Agda’s Ring Solver
    • Tactical Solving
    • The Pen and Paper Algorithm
    • Horner Normal Form
    • Multivariate Polynomials
    • Building a Semiring over HNF
    • Semantics
    • Syntax
    • Solving the Ring
    • Ergonomics
  • Bibliography
  • Acknowledgments
  • About the Author
  • Other Books by Sandy Maguire

The Leanpub 60 Day 100% Happiness Guarantee

Within 60 days of purchase you can get a 100% refund on any Leanpub purchase, in two clicks.

Now, this is technically risky for us, since you'll have the book or course files either way. But we're so confident in our products and services, and in our authors and readers, that we're happy to offer a full money back guarantee for everything we sell.

You can only find out how good something is by trying it, and because of our 100% money back guarantee there's literally no risk to do so!

So, there's no reason not to click the Add to Cart button, is there?

See full terms...

80% Royalties. Earn $16 on a $20 book.

We pay 80% royalties. That's not a typo: you earn $16 on a $20 sale. If we sell 5000 non-refunded copies of your book or course for $20, you'll earn $80,000.

(Yes, some authors have already earned much more than that on Leanpub.)

In fact, authors have earnedover $13 millionwriting, publishing and selling on Leanpub.

Learn more about writing on Leanpub

Free Updates. DRM Free.

If you buy a Leanpub book, you get free updates for as long as the author updates the book! Many authors use Leanpub to publish their books in-progress, while they are writing them. All readers get free updates, regardless of when they bought the book or how much they paid (including free).

Most Leanpub books are available in PDF (for computers) and EPUB (for phones, tablets and Kindle). The formats that a book includes are shown at the top right corner of this page.

Finally, Leanpub books don't have any DRM copy-protection nonsense, so you can easily read them on any supported device.

Learn more about Leanpub's ebook formats and where to read them

Write and Publish on Leanpub

You can use Leanpub to easily write, publish and sell in-progress and completed ebooks and online courses!

Leanpub is a powerful platform for serious authors, combining a simple, elegant writing and publishing workflow with a store focused on selling in-progress ebooks.

Leanpub is a magical typewriter for authors: just write in plain text, and to publish your ebook, just click a button. (Or, if you are producing your ebook your own way, you can even upload your own PDF and/or EPUB files and then publish with one click!) It really is that easy.

Learn more about writing on Leanpub