"formal methods" entries

Four short links: 19 April 2016

Four short links: 19 April 2016

Security Controls, Dataflow Checkups, Fair Use Wins, and Internet Moderators

  1. Security Controls for Computer Systems — Declassified 1970s DoD security document is still relevant today. (via Ars Technica)
  2. Checking Up on Dataflow Analyses — notable for a very easy-to-follow introduction to what dataflow analysis is. Long after the chatbot startups have flamed out, formal methods research in CS will be a key part of the next wave of software where code writes code.
  3. Fair Use Triumphs in Supreme Court (Ars Technica) — a headline I never thought I’d see in my lifetime. The Supreme Court let stand the lower court opinion that rejected the writers’ claims. That decision today means Google Books won’t have to close up shop or ask book publishers for permission to scan. In the long run, the ruling could inspire other large-scale digitization projects.
  4. The Secret History of Internet Moderators (The Verge) — the horrors and trauma of the early folks who developed content moderation systems (filtering violence, porn, child abuse, etc.) for Facebook, YouTube, and other user-contributed-content sites. It’s still a quiet and under-supported area of most startups. Some of them now meet roughly monthly for dinner, and I’m kinda glad I’m not around the table for that conversation!

(more…)

Four short links: 23 February 2016

Four short links: 23 February 2016

AI or IA, Retro Chatbots, Science by Software, and Spec as Test Oracle

  1. Doing Something For Me vs Allowing Me To Do Even More (Matt Webb) — nails the split in startups. Come on, valley kids … do you want diapers or do you want superpowers?
  2. Paul Ford on RacterBut don’t get too ahead of things. Using Racter is not as different from using Siri as you might expect. It’s just that Siri has petabytes of stuff in her brain, whereas Racter has a floppy’s worth. Computers have changed a ton in the last 30 years, humans barely at all. Don’t mistake their progress for ours. We’ve learned how to talk to computers, and they’ve learned how to pretend to understand us. Useful when driving. People love chatting with their Amazon Echo. But the conversation still doesn’t really mean anything.
  3. Accelerating Science: A Computing Research Agenda (PDF) — Siri thinks I want to tell telemarketers to “duck off,” while researchers look to automated hypothesis generation, experiment design, results analysis, and knowledge integration.
  4. Not Quite So Broken TLS (Adrian Colyer) — instead of ad-hoc codery, A precise and testable specification (in this case for TLS) that unambiguously determines the set of behaviours it allows (and hence also what it does not). The specification should also be executable as a test oracle, to determine whether or not a given implementation is compliant. The paper outlines this for TLS, but I see formal methods growing in importance in coming years. We can’t build an airport with cardboard on a swamp. In this metaphor, cardboard represents our ad hoc dev practices and the swamp is our platform of crap code. The airport is … look, never mind, I’ll work on the metaphor. Read the paper.