You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.
A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness.
In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers.
Bio
Jean Yang (@jeanqasaur) is a final-year PhD student at MIT. For her PhD thesis she has created Jeeves, a programming language for automatically enforcing information flow policies for security and privacy. You may be more familiar with one of her other projects, Haskell Ryan Gosling.
The text was updated successfully, but these errors were encountered:
@jeanqasaur
Sponsored by The Ladders (@TheLaddersDev)
This issue has been created to start/spark/organize a conversation on the paper An Axiomatic Basis for Computer Programming by C.A.R. Hoare.
Please offer up questions, comments, or additional information regarding this paper.
Paper can be found here or in the repo.
Description
Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.
A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness.
In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers.
Bio
Jean Yang (@jeanqasaur) is a final-year PhD student at MIT. For her PhD thesis she has created Jeeves, a programming language for automatically enforcing information flow policies for security and privacy. You may be more familiar with one of her other projects, Haskell Ryan Gosling.
The text was updated successfully, but these errors were encountered: