[ashtami8]

In the (is this shape fillable by 1x2 dominoes?) example given by EWD to demonstrate the power of formal reasoning methods, a slight change to the problem statement:

   For the shape Q, instead of clipping opposite corners of the 8x8 square board, one (what would lay under a) white square and one black square, which are non-adjacent, are randomly removed. 

makes the elegant proof argument fail.

Real world programming is usually like this, it is hard to cast the problem in the framework of a formal language, like first order predicate logic, and manipulation of uninterpreted formulae (i.e. the problem now mapped into the domain of first order logic) using the rules of first order logic might not lead to anything useful.

It seems to me that EWD is showcasing some example programming problems that are elegantly handled by his formal proof techniques, while ignoring the vast swathes of programming problems that might not be well handled by these techniques.

[Chinjut]

There is an extremely elegant solution to this modified question as well. In fact, it is always possible to fill a chessboard with dominoes with two squares of opposite color removed, by a very straightforward method (Gomory's Theorem). See Problem 2 at https://www.cut-the-knot.org/do_you_know/chessboard.shtml and note that the result generalizes to any bipartite Hamiltonian graph, such as any rectangular grid with an even number of cells.

(Much more generally, Hall's marriage theorem characterizes which finite bipartite graphs have a perfect matching, and there are polynomial-time algorithms to compute maximum cardinality matchings in arbitrary finite graphs.)

[carapace]

Essentially what you're arguing for is the desirability of untrustworthy software.

Typically people have insisted that it's too expensive to prove software correct, but as the machines and techniques improve proven-correct software becomes cheaper and cheaper.

The last argument standing is that it's unpopular.

[Pet_Ant]

On my current project the way totals and taxes are applied different on two different screens leading to slightly different totals. No one knows which one is actually correct or used by the customers in practice. Thus, you could say there is no correct answer.

Most software development is wrestling with malleable requirements.

As the old joke goes: writing software from requirements is like walking on water, both are easy when frozen

[ogogmad]

Note that in the adjacent case, a nice recursive algorithm can solve the problem.

What's the general solution in the random non-adjacent opposite-colour case, out of only the slightest curiosity?

[eigenket]

Write down a Hamiltonian cycle for the (undirected) graph where the nodes are given by the squares of the chessboard and are connected by edges if they are (orthogonally) adjacent. Notice that because the squares are different colors, deleting them from the Hamiltonian cycle partitions it into two even length paths. Cover each even length path with dominoes.

The part where you notice the two paths are even length feels a bit like dark magic the first time you see it. Notice that if you have two different coloured squares which are consecutive on the cycle the paths you get are length 64-2 and 0, then if as you move one of them further and further along the path you have to move in steps of 2 to keep them opposite colours.