5 ms·

How has this book helped you as a programmer? I am finding it difficult going through it.

alehul 9y ago
I'm currently taking a near-identical course as a CS freshman, and while I lack the programming expertise to adequately explain the importance in that field, it's definitely valuable to learn. I've never enjoyed a maths class more, really. It offers so many 'hacks' to working with numbers, which I could imagine would make code more efficient and avoid unnecessary computations when dealing with very large numbers. Separately, my increased mental efficiency with problems involving numbers is really surprising. There have been interview questions I've read about in the past where I've thought "someone must be a genius to be able to answer that through mental math," and it all makes so much more sense now! It's taught me about dozens of visualizations that can break down these problems in much more manageable ways. As an example of a mental maths problem on my midterm: How many numbers between 1 and 99,999 have digits that add up to 10? (23,500 would work whereas 23,510 would not). While initially I would have no clue how to answer this, learning about the balls-in-bins method solves it in an incredibly simple manner.
- deleted 9y ago
  [deleted]
smrk007 9y ago
I am also taking a course similar to this at my own university, actually using the same text-book. I guess the knowledge and skills gained from this course only apply to a small subset of problems, specifically those requiring some heavier theoretical / algorithmic thinking before implementation. While this only goes over a few algorithms in the chapters I have studied, it gives a very strong background which I'm sure would help in any other studies of algorithms you would pursue. Just by being introduced to the basic notation and language of some of the mathematics, I've found that I can read on different algorithms (in context of an academic paper / report) that I would like to implement with much more ease.
bitL 9y ago
Nearly 0 in practice. It's great if you want to get a CS PhD and off to high-paying jobs in SV/WS. Rite of passage mostly.
nickpsecurity 9y ago
I've been collecting some books on proof to build a foundation for better learning formal verification of software. The capabilities of modern provers, esp if combined with automated methods, can handle a lot more practical software than in the past. Even those like SPARK Ada with a lot of automation has properties that require manual proof. Certain things might also be easier to prove manually with a more powerful logic. My hope is that I find enough feedback on good/bad of cheap or free resources on this topic that I can determine some default recommendations for people curious. The problems can be addressed with supplementary material. Eventually, the defaults would be good enough that the process would happen faster. A larger number of people centering on the same resources might become a community for helping new people. That might increase the inflow. Simultaneously, some percentage of these people are working on tools, esp automated, to make the proof process more productive. Over time, we might have a much larger segment of people working on formal verification than we do now. Maybe even large enough to sustain more tool development by contributions or licensing. So, that's why I'm looking at books like this with what I think they might help us achieve. I'm way too out of my depth to know if it will work. I just know accessibility, better learning materials, and network effects always help. Example tools below for sequential programs, concurrency, and hardware: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) https://learntla.com/introduction/ https://learntla.com/introduction/ http://prod.sandia.gov/techlib/access-control.cgi/2014/1420533.pdf http://prod.sandia.gov/techlib/access-control.cgi/2014/14205...
- yannickmoy 9y ago
  I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification, this is well examplified by the document "ACSL by Example" about Frama-C: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it: https://github.com/yoogx/spark_examples/tree/master/spark-by-example https://github.com/yoogx/spark_examples/tree/master/spark-by... As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html http://docs.adacore.com/codepeer-docs/users_guide/_build/htm... https://docs.adacore.com/spark2014-docs/html/ug/en/source/gnatprove_by_example.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn... This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook https://ssearch.oreilly.com/?q=cookbook) the goals to get very concrete immediately, on code that the reader might have to write or have already written.
saagarjha 9y ago
In my experience, it's been helpful occasionally. I've used techniques from it once or twice when writing algorithms to figure out what exactly the constraints on their inputs would be, however, other than that I don't think I've ever used it.
rodorgas 9y ago
The text book says: "The analogy between good proofs and good programs extends beyond structure. The same rigorous thinking needed for proofs is essential in the design of criti- cal computer systems. When algorithms and protocols only “mostly work” due to reliance on hand-waving arguments, the results can range from problematic to catastrophic. An early example was the Therac 25, a machine that provided radia- tion therapy to cancer victims, but occasionally killed them with massive overdoses due to a software race condition. A more recent (August 2004) example involved a single faulty command to a computer system used by United and American Airlines that grounded the entire fleet of both companies—and all their passengers! It is a certainty that we’ll all one day be at the mercy of critical computer systems designed by you and your classmates. So we really hope that you’ll develop the ability to formulate rock-solid logical arguments that a system actually does what you think it does!"

I'm currently taking a near-identical course as a CS freshman, and while I lack the programming expertise to adequately explain the importance in that field, it's definitely valuable to learn. I've never enjoyed a maths class more, really. It offers so many 'hacks' to working with numbers, which I could imagine would make code more efficient and avoid unnecessary computations when dealing with very large numbers. Separately, my increased mental efficiency with problems involving numbers is really surprising. There have been interview questions I've read about in the past where I've thought "someone must be a genius to be able to answer that through mental math," and it all makes so much more sense now! It's taught me about dozens of visualizations that can break down these problems in much more manageable ways. As an example of a mental maths problem on my midterm: How many numbers between 1 and 99,999 have digits that add up to 10? (23,500 would work whereas 23,510 would not). While initially I would have no clue how to answer this, learning about the balls-in-bins method solves it in an incredibly simple manner.

deleted 9y ago
[deleted]

smrk007 9y ago

I am also taking a course similar to this at my own university, actually using the same text-book. I guess the knowledge and skills gained from this course only apply to a small subset of problems, specifically those requiring some heavier theoretical / algorithmic thinking before implementation. While this only goes over a few algorithms in the chapters I have studied, it gives a very strong background which I'm sure would help in any other studies of algorithms you would pursue. Just by being introduced to the basic notation and language of some of the mathematics, I've found that I can read on different algorithms (in context of an academic paper / report) that I would like to implement with much more ease.

bitL 9y ago

Nearly 0 in practice. It's great if you want to get a CS PhD and off to high-paying jobs in SV/WS. Rite of passage mostly.

nickpsecurity 9y ago

I've been collecting some books on proof to build a foundation for better learning formal verification of software. The capabilities of modern provers, esp if combined with automated methods, can handle a lot more practical software than in the past. Even those like SPARK Ada with a lot of automation has properties that require manual proof. Certain things might also be easier to prove manually with a more powerful logic. My hope is that I find enough feedback on good/bad of cheap or free resources on this topic that I can determine some default recommendations for people curious. The problems can be addressed with supplementary material. Eventually, the defaults would be good enough that the process would happen faster. A larger number of people centering on the same resources might become a community for helping new people. That might increase the inflow. Simultaneously, some percentage of these people are working on tools, esp automated, to make the proof process more productive. Over time, we might have a much larger segment of people working on formal verification than we do now. Maybe even large enough to sustain more tool development by contributions or licensing. So, that's why I'm looking at books like this with what I think they might help us achieve. I'm way too out of my depth to know if it will work. I just know accessibility, better learning materials, and network effects always help. Example tools below for sequential programs, concurrency, and hardware: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) https://learntla.com/introduction/ https://learntla.com/introduction/ http://prod.sandia.gov/techlib/access-control.cgi/2014/1420533.pdf http://prod.sandia.gov/techlib/access-control.cgi/2014/14205...

yannickmoy 9y ago
I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification, this is well examplified by the document "ACSL by Example" about Frama-C: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it: https://github.com/yoogx/spark_examples/tree/master/spark-by-example https://github.com/yoogx/spark_examples/tree/master/spark-by... As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html http://docs.adacore.com/codepeer-docs/users_guide/_build/htm... https://docs.adacore.com/spark2014-docs/html/ug/en/source/gnatprove_by_example.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn... This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook https://ssearch.oreilly.com/?q=cookbook) the goals to get very concrete immediately, on code that the reader might have to write or have already written.

saagarjha 9y ago

In my experience, it's been helpful occasionally. I've used techniques from it once or twice when writing algorithms to figure out what exactly the constraints on their inputs would be, however, other than that I don't think I've ever used it.

rodorgas 9y ago

The text book says: "The analogy between good proofs and good programs extends beyond structure. The same rigorous thinking needed for proofs is essential in the design of criti- cal computer systems. When algorithms and protocols only “mostly work” due to reliance on hand-waving arguments, the results can range from problematic to catastrophic. An early example was the Therac 25, a machine that provided radia- tion therapy to cancer victims, but occasionally killed them with massive overdoses due to a software race condition. A more recent (August 2004) example involved a single faulty command to a computer system used by United and American Airlines that grounded the entire fleet of both companies—and all their passengers! It is a certainty that we’ll all one day be at the mercy of critical computer systems designed by you and your classmates. So we really hope that you’ll develop the ability to formulate rock-solid logical arguments that a system actually does what you think it does!"