The Shape of Code

The original study saying formal verification was useless. In Section 6 of this paper [1], Avra Cohn gave a similar reality check when attempting to mechanize a hardware proof. Also, Guttman summarizes here [2] problems with many verification efforts. Finally, Wired has a modern take [3] on debate in 1979 paper by de Millo et al. These collectively represent most of opposition’ points to formal verification of software.

This is great for its description of social process of mathematics, the traditional approaches, and the limitations. I’m probably going to do a takedown of some points in the de Millo et al work at some point because I think the field got far enough to address some of it. There’s still some truth in what they’re saying. Probably best to treat new approaches as something different from traditional math with their own goals and expectations.

Any rebuttal of mine would focus on the LCF + de Bruijn approach negating much risk in proof steps, the high-level languages/frameworks that were built to make it easier (not easy), the fact that many people are doing what they suggest they won’t, the examples corroborating reliability benefits, and something exploring vetted theorems vs vetted verified components which I think are similar in how they’re used.

The risk that they predicted best was trusting verified components so much they didn’t include other checks: many ended up doing that. Good news is we have ways to do assurance in depth for those that are willing.…

I was just about to write a response to 'Scratch bashing' ;-). Luckily you have voiced most of them. So I'd like to add the following:

The Scratch programming environment, being the most child-friendly system I've ever seen so far (and I have tried to teach children, as well as adults with zero prior programming experience, using environments as different from each other as StarLogo and Python), lets children create amazing programs, but most important of all introduce the fundamentals of computational thinking and creativity with almost zero barriers for entry. From a programming perspective it definitely has a lot of shortcomings (most of which have been addresses by 'add-on's or similar systems built on top of it) but if you want to show the basics to a bunch of kids who are 7 or 8 year olds, then it is a great system.

Moreover, the social aspects of Scratch, namely easily publishing your projects and seeing the source code of others, are a gift. Try to do the same with Python and GitHub (one of my favorite combinations when I'm not dealing with children ;-), starting from scratch (some pun intended) and showing them all the tools... I'm curious how far their attention span would go.

Finally, apparently a number guessing game can be super easily implemented with a 'fake programming language' such as Scratch, too: http://scratch.mit.edu/projects/emres/2859373

And the source code, plain and simple, is probably easier to explain to children (and I had kids create much…

R is awful. It's full of decisions made by people who seem to not have much programming experience, in that they seem good at the time but cause major issues later on. See, for instance, http://www.talyarkoni.org/blog/2012/06/08/r-the-master-troll-of-statistical-languages/ , http://blog.revolutionanalytics.com/2008/12/use-equals-or-arrow-for-assignment.html , http://shape-of-code.coding-guidelines.com/2012/02/29/parsing-r-code-freedom-of-expression-is-not-always-a-good-idea/ , and the necessity of http://tim-smith.us/arrgh/ (I wrote up some stuff about the *apply functions, but not yet in a form suitable for the guide: https://github.com/tdsmith/aRrgh/issues/18 ) .

these folks were the first to push CASE tools, which are a footnote in software history because they failed rather completely in actual production usage. they invented COCOMO, which never gets used for the easy reason of routine order-of-magnitude margins of error (60% in studies, 600% in practice...). they were the biggest pushers or UML and graphical programming, which dies and lives again and again in increasingly zombified states...

have a dealie about cocomo specifically, I suppose.
http://shape-of-code.coding-guidelines.com/2016/05/19/cocomo-how-not-to-fit-a-model-to-data/

> 3) Why do you consider a 20 year old paper that's only been cited 16 times to be critical reading about estimation, when a vast body of research in forecasting exists, written by people who have measurements of the accuracy of estimates to base their theoretical models on?

Have some links to this vast body?

I've encountered very few over the years that actually qualify as "science" as much of it is fake or close to fake.

http://shape-of-code.coding-guidelines.com/2021/01/17/software-effort-estimation-is-mostly-fake-research/