Software Foundations | Hacker News Reader

Software Foundations

cis.upenn.edu

114 pointsluu14 comments

I cannot recommend this book enough. It is tough but highly rewarding. You will walk away from reading it, whether you complete it or not, with such a greater appreciation for types, for logic, for programming.

This is really relevant to my interests and I've been meaning to go through it for a while, but I can't seem to find much documentation on getting started with Coq (the actual using of it, like how to run the compiler, etc). I'm sure the information is out there, but it's at least enough of a PITA to keep me from getting started... :(

Have you looked at Adam Chlipala's Certified Programming with Dependent Types book? It uses Coq and Proof General. There's an online version: http://adam.chlipala.net/cpdt/

Allen, think it's time to switch to emacs ;)

Lol... I only use emacs if required to. Which, it seems, with Coq or Agda is the case. :(

Just download and use CoqIDE.

Learn You a Haskell is on my to do list and new books have appeared http://learnyouahaskell.com/

This hard-core type theory appears in the Univalent Foundations stuff from IAS this year. http://homotopytypetheory.org/book/

I love how the overview shows the dependencies for each chapter, very cool if you want to skip ahead to something interesting.

I've been running through this book as a self-study this semester. I'm currently on the Small-Step Semantics chapter.

This is bloody brilliant and I find it more relaxing and yet more enlightening than any course I've ever taken.

Qoc looks similar to Haskell. I have been learning Haskell for years. What would Qoc offer that Haskell doen't?

Coq is first and foremost a proof assistant, you can construct theorems in types and inhabitants of those types constitute proofs of theorems. it's based on a much more advanced type system called the Calculus of Constructions[1]. Coq is not suited for writing programs, though some people do use it to extract formally verified code in some highly specialized cases.

Haskell is a general purpose high-level language suitable for writing any kind of high-level program.

[1] http://en.wikipedia.org/wiki/Calculus_of_constructions

Wow I had this professor last semester. Great guy!

Who and what will benefit from this seemingly tough book?

Certainly people with 'turing' in their user names. I would have guessed.

Reply on news.ycombinator.com