[cctalk] Re: Getting floppy images to/from real floppy disks.

Yes. The problem is the gap between informal understanding and formal description. For many programmers, that gap occurs when the program source is created. If the programs are subjected to formal proofs, the gap occurs when the formal specs are written. So such things are largely a non-solution. They may help a little if the gap to the formal spec is smaller. If, as Guy is saying, the formal spec is larger than the code, then obviously that won't be the case. Languages other than C and C++ have advantages in that they detect, or avoid, a whole lot of bugs that C/C++ ignore, like bounds violations or memory leaks. So Ada can be helpful in that some bugs are harder or impossible to create, or more likely to be detected in testing. But, in spite of having taken a very interesting week-long course on program proofs by pioneer E.W. Dijkstra, I don't actually believe in those things. The 737MAX is a classic example of designers turning off their brains before doing their work. It is obvious even to me (who have never created safety-sensitive software) that you don't attach systems with single points of failure such as non-replicated sensors to a control system whose specific purpose is to point the airplane nose DOWN. If you do your work with your brain disabled you can't produce correct software, with or without formal proofs. paul