Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Mathematics for Computer Science: Readings

ocw.mit.edu

Post reply on HN
Print view View original

61–70 of 74 posts

Re: Mathematics for Computer Science: Readings

#61

Post by dsacco »

smadge wrote: post #57
dsacco wrote: post #45

Earlier quoted context omitted.

You would not typically find dedicated undergraduate courses for graph theory, probability theory or combinatorics, no. At the very least you wouldn't expect to see those until you hit 300 level, but most likely not until graduate courses. Discrete mathematics is a grab bag of topics, and it's more fair to say that a discrete math course pulls in selected topics from other areas than to say it provides a focused cove…

Strange, I have taken a 4 credit, one quarter class in both probability theory and combinatorics in my undergraduate math and computer science education.

That’s interesting. Do you mind if I ask what textbooks/materials you used?

Re: Mathematics for Computer Science: Readings

#64

Post by ginnungagap »

abhishekjha wrote: post #3
mikevm wrote: post #2

Latest edition of the book: https://courses.csail.mit.edu/6.042/spring18/mcs.pdf

I wonder how one would read 1000+ pages of a technical book like this.

From the introduction to Shelah's Classification Theory and the number of nonisomorphic models (an extremely technical book with 700+ pages):

  So we shall now explain how to read the book. 
  The right way is to put it on your desk in the day, below your pillow in the night,
  devoting yourself to the reading,
  and solving the exercises till you know it by heart.

Re: Mathematics for Computer Science: Readings

#65

Post by rodorgas »

sidcool wrote: post #18

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

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!"

Re: Mathematics for Computer Science: Readings

#66

Post by mannykoum »

smadge wrote: post #57
dsacco wrote: post #45

Earlier quoted context omitted.

You would not typically find dedicated undergraduate courses for graph theory, probability theory or combinatorics, no. At the very least you wouldn't expect to see those until you hit 300 level, but most likely not until graduate courses. Discrete mathematics is a grab bag of topics, and it's more fair to say that a discrete math course pulls in selected topics from other areas than to say it provides a focused cove…

Strange, I have taken a 4 credit, one quarter class in both probability theory and combinatorics in my undergraduate math and computer science education.

Me too. Discrete math was mainly combinatorics w/ an intro to probability. Then, probability theory was a separate requirement and, in addition to a Linear Algebra/ODE combo class, we had a CS theory class that covered Set theory, Proofs, Graph theory, TMs, etc. Most of these also had Math or Stats dept. equivalents.

These were our —typically— freshman/sophomore year CS classes (although I took a couple in my junior year) so I guess every school defines their requirements differently.

Re: Mathematics for Computer Science: Readings

#67

Post by yannickmoy »

nickpsecurity wrote: post #47
sidcool wrote: post #18

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

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 l…

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/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...

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/htm...

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) the goals to get very concrete immediately, on code that the reader might have to write or have already written.

Re: Mathematics for Computer Science: Readings

#68

Post by nickpsecurity »

yannickmoy wrote: post #67
nickpsecurity wrote: post #47

Earlier quoted context omitted.

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 l…

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/mast... This has inspired other researchers to do the same for SPARK, but…

It's funny you mention that because I've been collecting those Frama-C, SPARK, and WhyML papers in case anyone wants to port examples between languages. One of the things I [re-]downloaded a week or two ago for that was ACSL by Example. :) I also got floating point verification (I know you all are doing that), one on string functions, and one on GMP for big integers. I don't have any of it published in an online repo yet. I mostly just submit it to Lobste.rs for their crowd that likes deeper tech and give it to individual people via social media or email.

https://lobste.rs/newest/nickpsecurity

The stories section of that link has examples including recent ones on floating point and interior point. The interior point paper you might find interesting since they have a specific specification and coding style to achieve full automation.

https://hal.archives-ouvertes.fr/hal-01681134/document

You might also find Lea Wittie's work on Clay interesting. I was looking at her dissertation in case one could use SPARK in similar way to model I/O or concurrency.

https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf

re your concrete examples

I like that you're all doing that. That does help a lot. I plan to do my part to some degree in the near-ish future: I bought the High-Integrity Applications book for SPARK and Stavely's Toward Zero-Defect Programming for Cleanroom.

http://infohost.nmt.edu/~al/cseet-paper.html

SPARK book looks well-written but kind of packed with info esp on the language. Might take some time for me to learn. The Cleanroom book is highly approachable with the method mostly being algebraic focused on human understanding with symbolic-style verification of some control flow mechanisms. That was from a skim, though, with full method maybe being harder. My plan is to get back into feel of doing this stuff by trying Cleanroom first followed by using what SPARK book teaches me on all the same stuff. Both during and after learning SPARK, I'll use it on little functions like in the ACSL by Example book. Note that this assumes some other research doesn't take higher priority for me like my Brute-Force Assurance concept that mixes languages with their verification tooling.

I took the first steps of trying to get the SPARK GPL environment downloaded and installed. That wasn't working for some reason. It's harder than necessary to install: should be a well-packed installer like most things are on major Linux distros (esp Ubuntu) if wanting maximum adoption/experimentation. Since newest stuff from download link failed, I pulled older stuff through Synaptic which at least got GNAT working on doublec's Hello World example below. SPARK 2014 refused to run on it, though.

https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spa...

So, I gotta get SPARK working on my machine before trying to learn it. Sucks that it's been this difficult. I'll try again later this week.

Re: Mathematics for Computer Science: Readings

#69

Post by topologie »

codekilla wrote: post #34

Avi Wigderson's forthcoming book is pretty great if this sort of thing interests you: https://www.math.ias.edu/files/mathandcomp.pdf#page=1

It looks even better than the MIT course itself. I hadn't heard of Wigderson before, but now I'm definitely going to keep an eye on his work. Thank you for sharing this.

Re: Mathematics for Computer Science: Readings

#70

Post by yannickmoy »

nickpsecurity wrote: post #68
yannickmoy wrote: post #67

Earlier quoted context omitted.

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/mast... This has inspired other researchers to do the same for SPARK, but…

It's funny you mention that because I've been collecting those Frama-C, SPARK, and WhyML papers in case anyone wants to port examples between languages. One of the things I [re-]downloaded a week or two ago for that was ACSL by Example. :) I also got floating point verification (I know you all are doing that), one on string functions, and one on GMP for big integers. I don't have any of it published in an online repo…

Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they say "We worked with real variables to concentrate on runtime errors, termination and functionality and left floating points errors for a future work.") Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code.

Re learning SPARK, we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK, hopefully with online tweakable examples as on https://cloudchecker.r53.adacore.com/

With the SPARK Discovery GPL 2017 edition (from https://www.adacore.com/download), note that you'll get only Alt-Ergo installed by default. You need to follow these other instructions to add CVC4/Z3: http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/a...

If you have any problems, let's discuss on spark2014-discuss@lists.adacore.com, or report it on spark@adacore.com

I'm curious about your Brute-Force Assurance concept, can you say more?

Post reply on HN