Name: Programming in the 1990s
ISBN: 9780387973821

What Hacker News says

agentultraOct 2019

The Art of Computer Programming

Structure and Interpretation of Computer Programs

Purely Functional Data Structures

Programming in the 1990s

A Logical Approach to Discrete Math

thread

agentultraNov 2017

A more graduate-level book but one I found pleasing:

A Logical Approach to Discrete Mathematics: https://www.amazon.com/Logical-Approach-Discrete-Monographs-...

And a more pragmatic approach to the same material (with a lot of cross-over in terms of proof-style, etc):

Programming in the 1990s: http://www.springer.com/gp/book/9780387973821

But one I particularly enjoyed early on was written for liberal-arts level students of maths (who might've been traumatized by maths in the past):

Introduction to Graph Theory: https://www.amazon.com/Introduction-Graph-Theory-Dover-Mathe...

It will actually get you into writing proofs in set theory within the first couple of chapters.

thread

agentultraJun 2017

Programming in the 1990s by Edward Cohen. A rather practical introduction to the calculation of programs from their specifications. Plenty of introductions to computer programming involve guessing your program into existence. This is one of those rare books that give a solid, pragmatic approach (with examples) of developing software from solid, mathematically sound specifications and avoiding errors by design.

Even if you don't adopt formal methods in your day-to-day work (often we're not building sky-scrapers) it's a useful book to give you insight into the kinds of questions one should be asking and thinking about when designing software systems.

thread

agentultraMar 2017

In what way? I'm a human being full of intertwined contradictions and personal mythologies. I have many ways in which to be influenced.

I've read so many books and they've all left their impression on me one way or another; even the most boring drivel!

If by influenced you mean to imply, as a programmer, then I would say perhaps Programming in the 1990s if that counts as "non-technology." It's a book about maths and using logical proofs as a tool for creating specifications of computer systems. Prior to reading that book I had treated "software specifications," with the same reverence as a sketch on the back of a napkin. As far as I was concerned the only specification that mattered was the source code and the tests that exercise it. I feel as though that book has greatly changed the way I approach problems and how I think when I'm thinking about software.

thread

agentultraNov 2016

Programming in the 1990s by Edward Cohen is an interesting book for introducing software developers to a method of proof writing by way of predicate calculus. It's a book one can read from cover to cover.

The TLA+ book by Leslie Lamport is also an interesting read even if it is specific to a particular logic for creating specifications. Any of his talks on TLA+ are also good for a high-level overview of the why and a bit of the how as well.

thread

agentultraAug 2016

> But at that point, you need to start considering bugs in proofs.

If there's a flaw in your specification it is much more obvious than in your code. A high-level specification is usually built up from formal mathematics to model the execution of a system. If you use a model-checker it will take the specification of the model of your system and check that the invariants and properties you specify will hold across all possible executions of that model. If there is a problem in your specification it will be immediately obvious which cannot be said of computer programs.

In other words if you cannot see the error in your specification what makes you think you should be implementing it?

Now there is a long-held myth that we cannot verify the entire software stack... so what's the point?

You do not have to verify the entire software stack. A specification of a critical component is often sufficient. Take Paxos as an example: the author, Leslie Lamport, wrote the specification in TLA+. You can follow the mathematics to convince yourself of its efficacy or you can trust that the model checker is implemented correctly and will be sufficient for your purposes. The same is implied for a proof assistant. The point is that you do not need to assume these things are true: you can verify them by hand if you have to... the math will check out.

The same is true for other critical components of distributed systems. A single and even multi-threaded application on a single computer is difficult enough to reason about (what with multiple cores executing tasks out-of-order and sharing different levels of cache... it's almost like a tiny distributed system itself). Humans make terrible predictions of performance and correctness that fail time and again when they are benchmarked and profiled. It gets magnitudes worse in large, distributed systems and specifications are only a tool to manage thinking in those terms.

It's actually a tool for simplifying the development of such complex systems. I don't trust a consensus protocol or a lock-free algorithm if it is not accompanied by some sort of verifiable specification... not some hand-waving English prose, but a hard formal mathematical specification.

Do we still use these under-specified systems? Yes, sometimes. The trade-off being that the risk is acceptable and we design ways to tolerate failures as best as we can. However I will prefer a system that provides specifications for its key components.

On the myth of cost... it's true, thinking hard about your system up-front has a cost to it. Where and what you choose to specify will have some correlation to how much time you choose to spend. However the other component of the equation to consider is how critical is it to get this system correct? Another way to think about it is to consider what is the worst thing that could happen if your design contains a flaw.

This is obscenely easy to do in distributed systems. Our brains are not well enough equipped to imagine a model of our system and trace its execution and all of its state 49 steps deep. When confronted with such information many of us are not even capable of seeing the forest for the trees! We think, "Bah, that could only happen once in 250,000 executions.. it's not worth worrying about!" They don't realize that when you make that bet a couple of million times a minute then it's quite often you will see that error. Finding those kinds of traces postmortem is incredibly difficult... and why waste the time searching for that error when spending the extra time up-front will save you the headache down the road?

Yes it requires more work and it costs more at the beginning of a project... but if you cannot afford to spend it then know what you're getting yourself into and act accordingly.

I honestly believe that these mathematical tools can be taught to intermediate-to-advanced programmers who could use them to check their designs and help them write better software. It may seem intimidating but it's just booleans: there are only two possible values for any expression in predicate logic! In all seriousness the tools that are available today to do this work are becoming use-able by mere mortals and are not the eldritch scrawls of snooty ivory-tower academics.

You don't need to spend billions. You can learn TLA+ in a couple of weeks and start writing specifications in a month. There's a fairly slim tome called, Programming in the 1990s that demonstrates a practical technique for proofs that is digestible by programmers.

I say, "don't accept 'battle-tested' as the hallmark of a reliable system," because it says nothing about the underlying, undiscovered errors in the implementation (I made the mistake of using the word, bug, earlier... a habit I am trying to correct). All that buzz-word signifies is that the developers have attempted to implement a white-paper as best they could and wrote unit tests for the code they care about and used their customers to find the errors and edge-cases they didn't initially consider. While that is valuable to you after the fact you must be wary that you'll probably find some of those errors yourself. Hopefully the paper they based their critical sections on published a specification or proof. That's always a bonus... but you need to check these things.

Worse, someone might try to sell you on their distributed mutex based on their well-reasoned essay describing said algorithm... don't trust it unless you can check the model or understand the proof. It may sound reasonable but engineers don't build sky-scrapers without blueprints.

thread