Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend?

If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragraph executive summary and 10 is an entire Ph.D's worth of training. I'd probably be looking at a 2.5 to a 5.




Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background):

* Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/

* Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/

* FRAP (Chlipala): http://adam.chlipala.net/frap/

* Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking

* Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100

* Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/




Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: