Alcides Fonseca

It’s the year 2070. You are a 20 year recruit that is going to travel back in time 12-monkey style to try and save the world. You get to 2025, you find proof on a iPhone and you need to take a screenshot and send to a safe email address. Do you have a change at discovering how to take a screenshot?

The other day I was locked out of my car. I had my keys, but the key fob button wouldn’t work and neither would the little button on the door handle that normally unlocks the car. At this point, every action I had to take in order to get into the car required knowledge of a hidden control. Why didn’t I just use my key to get in? First, you need to know there is a hidden key inside the fob. Second, because there doesn’t appear to be a keyhole on the car door, you also have to know that you need to disassemble a portion of the car door handle to expose the keyhole.

Philip Kortum has a nice article on how this quest towards “clean” interfaces actually hurts usability.

I’ve recently come across novel approaches to typography, which given how much we are moving to digital, I find to be rarer than expected.

Alternative Layout System presents different ways of justifying text or, in the case of the picture below, ways of annotating what is coming in the next line to help reading.

Kermit is a new font designed by Underwear and commissioned by Microsoft that aims to help kids to read, including those with dyslexia. But for me, it’s much more than that. It allows to include tones in the typography that help to convey how you should read some text, making kids books much more fun.

And don’t miss Jason Santa Maria’s other recommendations.

It seems to us that the scenario envisioned by the proponents of verification goes something like this: The programmer inserts his 300-line input/output package into the verifier. Several hours later, he returns. There is his 20,000-line verification and the message “VERIFIED.”

— Social Processes and Proofs of Theorems and Programs by Richard DeMillo, Richard Lipton and Alan Perlis

Although this is another straw man, many people claim to have verified something, offering as evidence a formal proof using their favourite tool that cannot be checked except by running that very tool again, or possibly some other automatic tool. A legible formal proof allows a human reader to check and understand the reasoning. We must insist on this.

— Lawrence C Paulson

In my research group, we have been thinking not only on how to improve error messages, but also how to improve the understandability of proofs. It feels good to read such reinsuring take.