Outerwear Edit from Shopbop
To share your reaction on this item, open the Amazon app from the App Store or Google Play on your phone.
Add Prime to get Fast, Free delivery
Amazon prime logo
$38.22
FREE Returns
FREE delivery Tuesday, January 28
Or Prime members get FREE delivery Saturday, January 25. Order within 2 hrs 4 mins.
Only 1 left in stock - order soon.
$$38.22 () Includes selected options. Includes initial monthly payment and selected options. Details
Price
Subtotal
$$38.22
Subtotal
Initial payment breakdown
Shipping cost, delivery date, and order total (including tax) shown at checkout.
Ships from
Amazon
Amazon
Ships from
Amazon
Returns
30-day refund/replacement
30-day refund/replacement
This item can be returned in its original condition for a full refund or replacement within 30 days of receipt.
Read full return policy
Payment
Secure transaction
Your transaction is secure
We work hard to protect your security and privacy. Our payment security system encrypts your information during transmission. We don’t share your credit card details with third-party sellers, and we don’t sell your information to others. Learn more
Kindle app logo image

Download the free Kindle app and start reading Kindle books instantly on your smartphone, tablet, or computer - no Kindle device required.

Read instantly on your browser with Kindle for Web.

Using your mobile phone camera - scan the code below and download the Kindle app.

QR code to download the Kindle App

Follow the author

Daniel P. Friedman
Follow
Something went wrong. Please try your request again later.

The Little Prover (Mit Press) 1st Edition

by Daniel P. Friedman (Author), Carl Eastlund (Author), Duane Bibby (Illustrator)
4.6 4.6 out of 5 stars 29 ratings
See all formats and editions
off. Enter code INSTAPAY10 at checkout. Discount by Amazon. Terms  off. Promo code INSTAPAY10 is saved to your account. Discount by Amazon. Terms  
{"desktop_buybox_group_1":[{"displayPrice":"$38.22","priceAmount":38.22,"currencySymbol":"$","integerValue":"38","decimalSeparator":".","fractionalValue":"22","symbolPosition":"left","hasSpace":false,"showFractionalPartIfEmpty":true,"offerListingId":"Yh04Rs7%2BVBzqYDhWm22%2F5d%2F69Yj%2F8l86HVilVe0i2S%2BPj9DxbbSNfvbkk3vXB%2BgWLVG3eSxzGmheyklcOyMCt0dTYM7AoKdQFuDk2%2BKZiuMhx05%2BuFirwpKEJ5aUgV%2BdNYS6Tbe%2FK6fEyM1s25Svswmb7lXLF99ZbKR7TWUJXXd1PExRo0ugVF9%2BVInghMEb","locale":"en-US","buyingOptionType":"NEW","aapiBuyingOptionIndex":0}]}

Purchase options and add-ons

An introduction to writing proofs about computer programs, written in an accessible question-and-answer style, complete with step-by-step examples and a simple proof assistant.

The Little Prover introduces inductive proofs as a way to determine facts about computer programs. It is written in an approachable, engaging style of question-and-answer, with the characteristic humor of The Little Schemer (fourth edition, MIT Press). Sometimes the best way to learn something is to sit down and do it; the book takes readers through step-by-step examples showing how to write inductive proofs. The Little Prover assumes only knowledge of recursive programs and lists (as presented in the first three chapters of The Little Schemer) and uses only a few terms beyond what novice programmers already know. The book comes with a simple proof assistant to help readers work through the book and complete solutions to every example.

Previous slide of product details
  1. ISBN-10
    0262527952
  2. ISBN-13
    978-0262527958
  3. Edition
    1st
  4. Publisher
    The MIT Press
  5. Publication date
    July 10, 2015
  6. Language
    English
  7. Dimensions
    8.9 x 6.9 x 0.5 inches
  8. Print length
    248 pages
  9. See all details
Next slide of product details

Frequently bought together

The Little Prover (Mit Press)
This item: The Little Prover (Mit Press)
$38.22
Get it as soon as Tuesday, Jan 28
Only 1 left in stock - order soon.
Sold by Ibook USA and ships from Amazon Fulfillment.
+
The Little Typer (Mit Press)
$54.00
Get it as soon as Tuesday, Jan 28
Only 4 left in stock - order soon.
Sold by Ibook USA and ships from Amazon Fulfillment.
+
The Reasoned Schemer, second edition (Mit Press)
$40.00
Get it as soon as Tuesday, Jan 28
Only 14 left in stock - order soon.
Ships from and sold by Amazon.com.
Total price: $00
To see our price, add these items to your cart.
Details
Added to Cart
spCSRF_Treatment
Some of these items ship sooner than the others.
Show details Hide details
Choose items to buy together.

Editorial Reviews

About the Author

Daniel P. Friedman is Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); and The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann).

Carl Eastlund is a software engineer at Jane Street Capital in New York City.

Matthias Felleisen is Trustee Professor in the College of Computer Science at Northeastern University.

Product details

  • Publisher ‏ : ‎ The MIT Press; 1st edition (July 10, 2015)
  • Language ‏ : ‎ English
  • Paperback ‏ : ‎ 248 pages
  • ISBN-10 ‏ : ‎ 0262527952
  • ISBN-13 ‏ : ‎ 978-0262527958
  • Reading age ‏ : ‎ 18 years and up
  • Grade level ‏ : ‎ 12 and up
  • Item Weight ‏ : ‎ 1.05 pounds
  • Dimensions ‏ : ‎ 8.9 x 6.9 x 0.5 inches
  • Customer Reviews:
    4.6 4.6 out of 5 stars 29 ratings

About the author

Follow authors to get new release updates, plus improved recommendations.
Daniel P. Friedman

Daniel P. Friedman

Brief content visible, double tap to read full content.
Full content visible, double tap to read brief content.

Daniel P. Friedman has been a Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University for nearly half a century and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann); and The Little Typer (with David Christiansen).

Customer reviews

4.6 out of 5 stars
29 global ratings

Review this product

Share your thoughts with other customers
Write a customer review

Top reviews from the United States

  • Herbert C. Meyer
    5.0 out of 5 stars how do you know...
    Reviewed in the United States on October 13, 2017
    Verified Purchase
    if your software is "correct" (whatever the hell that means) ? Usually you don't. If you care, you might say "it has passed every test I could think of, and had time to perform."
    This is not enough. The only way to prove (yep, prove) that your software is correct is to turn your program into a theorem, and prove the theorem. This approach is called Hoare Logic, after Tony Hoare. If you do not know who Tony is, go find out, before you write another program.
    Anyway, this text is an introduction to a proof assistant, a software tool to help you prove theorems. You hate proving theorems. I hate proving theorems. If I liked proving theorems, I would be a Mathematician. I am a Mathematician, and I hate proving theorems. Which is why I wrote software for a living, instead of proving theorems. Now I need to prove theorems to show my software works. I should have been a Physicist.
    40 people found this helpful
    Helpful
     Report
  • Roger Barraud
    5.0 out of 5 stars Five Stars
    Reviewed in the United States on November 25, 2017
    Verified Purchase
    A worthy continuation ( ;-) ) of the series... looking forward to playing with this using my new Scheme.
    3 people found this helpful
    Helpful
     Report
  • Michael Vanier
    5.0 out of 5 stars An accessible introduction to theorem proving in software
    Reviewed in the United States on April 26, 2016
    Disclaimer: I was a tech reviewer for this book.

    Ever since computer programming was invented, bugs have been the bane of every programmer's existence. But does it have to be that way? What if we could prove our programs correct? Computer-aided theorem proving applied to proving programs correct has a long and rich history, and its use has accelerated greatly over the past decade. I believe that this will be a foundational subject for the next generation of programmers, as the type systems for existing languages reach their limits and are replaced by richer type systems which require theorem provers as an integral part of the programming process. (Languages/environments like Agda, Coq, and Idris are exploring this space already.) The Little Prover is a very accessible introduction to theorem proving; if you understand the first few chapters of The Little Schemer (and are willing to work!) you will be able to follow The Little Prover. In addition, the material is fascinating in its own right and will be worthwhile reading as brain food for programmers looking for a new challenge (much like the other "Little" books that Friedman et al have written). However, don't confuse "accessible" with "easy". Compared to a lot of modern proof assistant software like Coq, the proofs are quite manual and require a lot of user guidance. This is actually advantageous in a book like this, because you see every step and never have to wonder how we got from point A to point B (plus the authors are doing all the hard work; you just have to follow along!). The authors also provide a downloadable proof assistant which is extremely helpful when the proofs get sufficiently complex, and they list all the proofs in their final form in the back of the book.

    I suspect that for most readers, the biggest conceptual hurdle will not be the material presented but just wrapping your head around the very notion that programs are something that can be reasoned about rigorously and that it is in fact possible to prove things about them. This is not the way we have been taught to think about programming, and it's not the way that programming is currently done. But it is the way that programming will have to be done in the future if we ever want to dig ourselves out of the swamp of perpetually-buggy software, and this book is an excellent starting point for learning about theorem proving in software. If you make it all the way to the end, I think you will be "proof-infected" and this will not be the last book on theorem proving that you read!
    9 people found this helpful
    Helpful
     Report
  • Bob Robert
    4.0 out of 5 stars Four Stars
    Reviewed in the United States on October 3, 2015
    Verified Purchase
    I haven't read it but I'm sure it's good. Friedman's other books are.
    One person found this helpful
    Helpful
     Report
  • D. Buchanan
    5.0 out of 5 stars A fun and enlightening introdution to computational logic.
    Reviewed in the United States on August 23, 2015
    The Little Prover is a great introduction to computation logic. I really enjoy it because of its format, its pacing, and its ability to explain core concepts in mathematics and computer programming.

    I like The Little Prover's question-and-answer format. It encourages me to write and understand proofs for myself, because the format explains the steps when I get stuck, and it helps me understand the significance of the steps when I succeed.

    The Little Prover was very well paced. More complicated proofs are introduced at a rate that keeps them challenging and interesting but never impossible.

    The way The Little Prover covers computational logic means I am able to relate it to my A-Level standard knowledge of proof in mathematics (A-Levels are the English equivalent of American high school). The book doesn't just show you how to use a computer program to do certain things, but relates what you're doing to concepts like inductive proof and recursion.

    The format of The Little Prover is very similar to the other books in the Little series such as The Little Schemer. I highly recommend those too. The Little Prover also contains many ideas found in How to Design Programs (HtDP). For example the programs in The Little Prover clearly all use design recipes from HtDP and concepts such as natural recursion are mentioned in both HtDP and The Little Prover.
    34 people found this helpful
    Helpful
     Report

Top reviews from other countries

  • Ignacio Blasco Lopez
    5.0 out of 5 stars They did it again
    Reviewed in Spain on January 5, 2017
    Verified Purchase
    Great and insightful, as usual. I've purchased another book in the series and they still keep high quality. I heartfully recommend it.
    Report
  • Peter Krumins
    5.0 out of 5 stars I was so excited that I pre-ordered a bunch of copies not just for myself but for all my friends!
    Reviewed in Germany on July 6, 2016
    Verified Purchase
    The Little Prover was published just a few months ago and when I learned it's getting published I pre-ordered a bunch of copies not just for myself but for all my friends. I was that excited!

    The Little Prover teaches the readers how to determine facts about recursive functions using induction. The book starts with programming concepts such as recursive functions and lists, and leads the reader along the shortest path to inductive proofs. It assumes knowledge of neither logic nor mathematics beyond arithmetic. Just like all other books in the series, it's written as a dialog between the authors and you in a super fun style with a lot of jokes and insider references. This book will make you think from page one and it will stretch your mind quite a bit.

    You'll learn about axioms, theorems, what it means for something to be true in computing, conjectures, claims, counterexamples, total functions, partial functions, conjunctions, induction, natural recursion, and more.

    While working through this book, you'll need j-bob, the proof assistant:

    [...]

    (Google for j-bob if this link gets removed.)

    You'll truly appreciate this book only after having read the other books in the series (The Little Schemer, The Seasoned Schemer, The Reasoned Schemer, The Little MLer). Get those first, and then read this book. And then read all the books again for full effect.

    I've placed this book #24 in my Top 100 Programming, Computer and Science books list:

    [...]

    (If this link gets removed google for >>catonmat top 100 programming computer science books<< to find my article.)

    .
    Report
  • Cleo
    5.0 out of 5 stars The Little Prover is Big Fun
    Reviewed in the United Kingdom on October 21, 2015
    Verified Purchase
    Great fun! Excellent service. Thank you!
    Report