Philosophy

Author’s note: I wrote this in 2017 and it languished in the drafts since then because I couldn’t think of a good conclusion. Really this is typical of the subject matter and all this piece offers is something to chew on, if you have the interest in it or have never before considered the question. At the time I was helping tutor a TLA⁺ seminar and had the opportunity to ask Leslie Lamport (who has thought about computation quite a bit! [Read More]

Why are we here? What guarantees does formal verification provide? This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all! What do we mean by software correctness? There are precisely two different ways for a piece of software to be correct: The supreme deity of the universe descends from the heavens and decrees, with all the weight of Objective Truth, that a certain piece of software is correct. [Read More]