CbyC is invaluable in avoiding errors in reasoning about formal models. But the relationship of a formal model---whether of a computer or of the real world of a cyber-physical system---may be a more prolific source of faiure. Recent posts cited the 737Max8 disasters. Were these due to formal errors in MCAS code? -- Michael Jackson