Jean Yang on An Axiomatic Basis for Computer Programming

Meetup: http://www.meetup.com/papers-we-love/events/214400572/ Paper: http://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf Slides: https://speakerdeck.com/paperswelove/jean-yang-on-an-axiomatic-basis-for-computer-programming Audio: http://www.mixcloud.com/paperswelove/jean-yang-on-an-axiomatic-basis-for-computer-programming/ --------------------------------------------------------------------------------------------- Sponsored by The Ladders (@TheLaddersDev) --------------------------------------------------------------------------------------------- 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.

Related Talks

ECMAScript 6 & Web Components • Brian LeRoux

This presentation was recorded at GOTO Chicago 2015 http://gotochgo.com Brian LeRoux - PhoneGap Project Team, Adobe ABSTRACT JavaScript has a long history of being difficult to structure and maintain. To deal with this complexity a swath of frameworks appeared over the years. Prototype.js was quickly followed by jQuery and hounded by Dojo, YUI, Mootools ...

Eric Shull: Communicating Sequential Processes (September 22, 2015)

The time has come to think concurrently. Traditional software concurrency management leads to non-deterministic race conditions and deadlocks that are hard to reproduce and debug, leading to unreliable software. That means it's time to introduce math. Tony Hoare's paradigm of communicating sequential processes, or CSP, is not only a robust ...

User Interface (UX) Techniques • Janne Jul Jensen

Check out our upcoming conferences at http://gotocon.com Subscribe to the GOTO Conferences YouTube Channel at https://www.youtube.com/user/GOTOConf... Janne Jul Jensen - Interaction Designer and Usability Specialist ABSTRACT Most developers today are aware of the importance of creating a good user interface with a high level of usability, but many are lacking the methods and techniques ...

Power Use of UNIX • Dan North

Dan North - Agile Troublemaker, Developer, Originator of BDD ABSTRACT Thus begins an old, and sadly lost in the mists of Usenet, love story about Vi and Ed (who becomes her "ex"), told entirely in Unix commands. I had no idea when I started learning these arcane (guess how the "dd" command ...

Speed & Scale: How to get there • Adrian Cockcroft

This presentation was recorded at GOTO Chicago 2014 http://gotochgo.com Adrian Cockcroft - Technology Fellow at Battery Ventures and Former Netflix Cloud Architect Pioneer ABSTRACT To deliver software products at high velocity requires four things. First, a culture of innovation that can see and respond to opportunities. Second, the data and analytics to evaluate alternatives. ...

Syntaxation • Douglas Crockford

Check out our upcoming conferences at http://gotocon.com Subscribe to GOTO Conference's YouTube Channel at http://www.youtube.com/user/GOTOConferences?sub_confirmation=1 Douglas Crockford - JSON Creator & Yahoo! JS Architect ABSTRACT Much of programming language design is dictated by fashion. As a consequence, opinions about programming languages tend to be strong, shallow, and deeply emotional. The best languages are brilliant ...

Fun with the Lambda Calculus • Corey Haines

This presentation was recorded at GOTO Chicago 2015 http://gotochgo.com Corey Haines - Author, Speaker, Teacher & all around Groovy Guy ABSTRACT You've probably heard about the lambda calculus, building up our computing structures from just the treasured lambda. But how much have you played with it? In this talk, armed only with Vim and ...

John Papa - 10 AngularJS Patterns - Code on the Beach 2014

Learn from John Papa's talk "10 AngularJS Patterns" from Code on the Beach 2014 at One Ocean Resort & Spa, Atlantic Beach, Florida. Sunday, August 10, 2014. www.codeonthebeach.com Abstract: "Once you get beyond the AngularJS basics there are many decisions to be made on how to build robust and maintainable apps. Come ...

Droidcon Montreal Jake Wharton - A Few Ok Libraries

Droidcon had its first Canadian edition on April 9-10, 2015 in Montreal. It was organized by Mirego http://www.mirego.com/en We had Jake Wharton telling us more about some Ok Libraries at Droidcon Montreal. A Few "OK" Libraries: This talk will be an in-depth look at Okio—a tiny library for interacting with bytes—and a ...

Kicking the Complexity Habit • Dan North

This presentation was recorded at GOTO Chicago 2014 http://gotochgo.com Dan North - Agile Troublemaker, Developer, Originator of BDD ABSTRACT Without rigorous care and attention software quickly becomes messy and unmanageable. Even with the best intentions entropy and complexity are a fact of life in growing applications. As in many other contexts it is easier ...