> I disagree. Prose based proofs can just as rigorous as proofs using code, or mathematical notation or images. You can use pictures in your proofs if you want

> I disagree. Prose based proofs can just as rigorous as proofs using code, or mathematical notation or images. You can use pictures in your proofs if you want. But the proofs have to be about the actual program you have written, rather than some pseudocode claimed without justification to be equivalent to it. > Why is it easier to use a language like Java to formulate a proof exactly? Proofs are written in the language of mathematics, not Java or any other programming language. However, Java programs are easier to prove things about than JavaScript programs because Java has a richer static semantics that you can use to discharge parts of your proof obligation simply by checking whether your code is a legal Java program. For instance, you can associate to each final class a set of object invariants, defined in terms of its public methods. Java's static semantics is not powerful enough to actually establish these object invariants (you have to do that yourself), but it is powerful enough to prevent users of a final class from breaking invariants that have been established by its implementor (provided users don't use certain misfeatures of the Java language, like reflection). > What are we talking about proving? The abstract algorithms being implemented or the implementations themselves? Both. A high-level programming language ought to allow you to express algorithms directly, without distracting you with irrelevant details. (Of course, Java doesn't always do this.)