3 ms·
> 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
by jlelonm 8y ago
> 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.
- nextos 8y agoSome 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/ https://softwarefoundations.cis.upenn.edu/ * Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/ http://www21.in.tum.de/~nipkow/Concrete-Semantics/ * FRAP (Chlipala): http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ * Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking * Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100 https://www.springer.com/gb/book/9783540654100 * Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/