What do you think?
Rate this book
Software Foundations #1
Software Foundations, Volume 1: Logical Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
Logical Foundations serves as the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq.
Logical Foundations serves as the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq.
325 pages, ebook
Published September 6, 2017
8 people are currently reading
111 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 6 of 6 reviews
September 21, 2019
alright, i'm calling it! several exercises had to be regrettably skipped, a few of them central, but i'll have to return when i have more experience. I'm much stronger now than I was before i started the book! and my mind is full of ideas of things i could try doing with Coq.
I'm also stronger at non-constructive proofs than i was before starting this.
It's such an easy book to love because it feels like a videogame! and I cant emphasize enough the value of doing exercises with such immediate feedback, to know for sure that you're really right or wrong and, unlike everywhere else in mathematics, to know for sure that you're not just dealing in opinions.
some notes about going through this-- optional chapters are quick and easy so you might as well do them. The biggest bottlenecks are Logic.v and IndProp.v, to some extent Tactics.v and Imp.v are bottlenecks as well. You have to be prepared to move at a glacial pace sometimes, depending on how many exercises you're willing to sacrifice. Once I estimated that my grade, if i was taking the course at Penn, would be like a B- or C i started moving a lot faster.
starting level: this is hard to determine. experience with nonconstructive math makes constructive math more gentle, for sure, but i doubt its impossible to dive into this fully green. I had by my side How to Prove It, a nonconstructive intro text, to review certain things, and that helped a moderate amount once or twice when things picked up speed in the Logic.v chapter. If you haven't done the basic lazy list recursion suite (map zip fold etc) you could use this as your introduction, and if you have done it a particular chapter or two will be trivially easy. At the end of the day, i don't know how to say who should read this exactly, except that i would default to everyone ought to. you gotta be willing to bleed tho-- it's hard sometimes!! I don't have professional software experience so i can't (credibly) say that the book is at all relevant to the real world, so i'll say this--- if you pursue the craft as orthogonal to the real world, we know at least that this book is for you (and, for all i know, it has real world benefits as well, but those are secondary).
Now what--- do i finish the haskell textbook i abandoned last year or do i go on to further volumes of SF? EDIT: i chose the haskell book.
Reading this book really drove home the meaning of marginal value (of exercises), because I sharpened my intuitions for when its ok to skip exercises. The benefit of completing an exercise is a marginal value-add, and when an exercise stops you like a wall you have to decide if that value is worth more than the value of continuing through the book. I think the result is that a number emerges, say 120 minutes for example, a ceiling on the amount of time you should spend on an exercise before it becomes not worth the opportunity cost.
I'm also stronger at non-constructive proofs than i was before starting this.
It's such an easy book to love because it feels like a videogame! and I cant emphasize enough the value of doing exercises with such immediate feedback, to know for sure that you're really right or wrong and, unlike everywhere else in mathematics, to know for sure that you're not just dealing in opinions.
some notes about going through this-- optional chapters are quick and easy so you might as well do them. The biggest bottlenecks are Logic.v and IndProp.v, to some extent Tactics.v and Imp.v are bottlenecks as well. You have to be prepared to move at a glacial pace sometimes, depending on how many exercises you're willing to sacrifice. Once I estimated that my grade, if i was taking the course at Penn, would be like a B- or C i started moving a lot faster.
starting level: this is hard to determine. experience with nonconstructive math makes constructive math more gentle, for sure, but i doubt its impossible to dive into this fully green. I had by my side How to Prove It, a nonconstructive intro text, to review certain things, and that helped a moderate amount once or twice when things picked up speed in the Logic.v chapter. If you haven't done the basic lazy list recursion suite (map zip fold etc) you could use this as your introduction, and if you have done it a particular chapter or two will be trivially easy. At the end of the day, i don't know how to say who should read this exactly, except that i would default to everyone ought to. you gotta be willing to bleed tho-- it's hard sometimes!! I don't have professional software experience so i can't (credibly) say that the book is at all relevant to the real world, so i'll say this--- if you pursue the craft as orthogonal to the real world, we know at least that this book is for you (and, for all i know, it has real world benefits as well, but those are secondary).
Now what--- do i finish the haskell textbook i abandoned last year or do i go on to further volumes of SF? EDIT: i chose the haskell book.
Reading this book really drove home the meaning of marginal value (of exercises), because I sharpened my intuitions for when its ok to skip exercises. The benefit of completing an exercise is a marginal value-add, and when an exercise stops you like a wall you have to decide if that value is worth more than the value of continuing through the book. I think the result is that a number emerges, say 120 minutes for example, a ceiling on the amount of time you should spend on an exercise before it becomes not worth the opportunity cost.
January 30, 2025
Very fun to work through the exercises. It was cool to be able to prove some core math/cs topics formally. One highlight was proving the pumping lemma for regular expressions. Some of the automation stuff didn't fully internalize yet. I'll continue onto volume 2 eventually, but for now I will take a break.
This entire review has been hidden because of spoilers.
March 13, 2022
This book is the first in a series about writing correct software. The title might fool you into thinking it is an introduction to programming style book, but it is not. The book starts with relatively simple examples. First you will programmatically prove some basic properties about natural numbers and array lists. By the end of the book you will find yourself implementing a full interpreter for a variation of while language. You will then prove some interesting properties about code written in that language such as termination for example.
I think this one of the best, if not the the best first book on the topic of formal methods for computer scientists and engineers alike.
I think this one of the best, if not the the best first book on the topic of formal methods for computer scientists and engineers alike.
August 30, 2021
The best programming book I've ever read in my life.
December 18, 2024
There are many hidden gems in the advanced exercises, both theoretical and practical. Don't just skip them.
May 18, 2020
Difficult and rewarding
Displaying 1 - 6 of 6 reviews