After reading the whole article, it seemed impressive .. Although didn't like his way of writing so simple ideas in a very very very long article. Anyway, TLA+

After reading the whole article, it seemed impressive .. Although didn't like his way of writing so simple ideas in a very very very long article. Anyway, TLA+ and Formal Methods seem a promising thing and definitely need to check that out. I totally agree with him with the way we are not giving a good weight to planning especially for applications that need robust security and safety. Especially after the appearance of Agile methodology and alike. (no system is perfect anyway) But definitely we need more of that verification and we don't need it in the esoteric way they mentioned but in the easy way that allows every programmer to use without so much complexity. Maybe tooling around something like TLA+ could make it easier to understand. People in here though say that it's not that hard but it's not beneficial in every single situation just when you have complex algorithms. I got convinced though with another idea that's easier to apply at least for now, using type systems (type theory) through using a programming language with sound type system (Facebook is making nice progress in that) on the front end FB made ReasonML , a language derived from OCaml to generate javascript. It really erases a whole set of bugs by getting a good type system like that. I'm learning these days OCaml and Reason. New languages as Rust are doing great too. I think writing code is improving these days but it'll get definitely better in the future as we understand more about how we actually do it. The field is just around 70 years old and it's still in its infancy I think.