5 ms·
An Axiomatic Basis for Computer Programming (1969) [pdf]
- BruceEel 6y agoA gem of readability and clarity.
- cjohansson 6y agoHow does one read it? I simply can't read it, only see the first page
- d_tr 6y agoDid you try more than one viewer? It renders fine in Evince and in Vivaldi here. The 'bodies' of the pages are not regular text but images over that background gradient, by the way.
- deleted 6y ago[deleted]
- baxrob 6y agoWorks for me but found this less unusual pdf: http://www.cs.toronto.edu/~chechik/courses05/csc410/readings/hoare_axiomatic.pdf http://www.cs.toronto.edu/~chechik/courses05/csc410/readings...
- tjalfi 6y ago(submitter) Thanks, I have asked dang to update the link.
- jasperry 6y agoThanks for posting this--I'm getting back into studying the formal semantics of programming languages. Questions for those working in this area: According to Pierce's Types and Programming Languages, axiomatic semantics of the type that Hoare pioneered are not found as useful today as operational semantics. Is that (still) true? Are the major approaches (operational, denotational, axiomatic) pretty much solidified now, or are there significant new efforts at finding better overall formalizing frameworks?
- auggierose 6y agoThere is only one formalising framework, it is called math. The rest is just noise. When trying to make a better framework for formalising computer programs, just make a better framework for formalising math first.
- taeric 6y agoMath has many formalisms. Some more useful than others, in certain contexts. All restricted by the norms of communication that they are written in. So, yes, there are some math formalities for processes. No, they probably don't help in finding new processes as much as you'd think. Despite being quite good at understanding existing processes through formal exploration.
- Joker_vD 6y agoYou can't make a better framework for formalising math, because, as you've yourself said, "there is only one formalising framework", and it's math itself. Cue the problems with self-application and Goedel's tricks :)
- auggierose 6y agoYeah, in a way you are right. Ok, let me put it this way: Math is not formal. But, formality has its advantages, so what I would like to see is a framework that, while being formal, still allows formulating ideas just as a mathematician would. Kind of like envisioned here: https://www.practal.com https://www.practal.com
- Joker_vD 6y agoRight, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done. The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.
- dang 6y agoHoare's thoughts on the 40th anniversary: https://cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext https://cacm.acm.org/magazines/2009/10/42360-retrospective-a... Discussed (barely) at the time: Retrospective: An Axiomatic Basis for Computer Programming - https://news.ycombinator.com/item?id=905176 https://news.ycombinator.com/item?id=905176 - Oct 2009 (1 comment)
- rramadass 6y agoAlso read Robert Floyd's paper Assigning Meanings to Programs. After getting the gist of the above, reading Bertrand Meyer's Design by Contract and Applying Design by Contract will clarify on how to apply the ideas to "real" systems.