Comment by WJW
> We can take a definition of a rose from a neural network that recognizes what a rose is
Can we? That just shifts the problem to building such a NN.
I think it would already be pretty tricky to get a decent sized panel of humans to agree on what a "rose" is. Do rose-shaped but yellow flowers count? How about those genetically altered thornless ones? How about perfectly imitatations that are made of plastic? Images of roses? The flowers from the list at https://www.epicgardening.com/rose-lookalikes/?
And of course there's the problem of getting a NN to recognise just roses. The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications. I very much doubt humanity could build a neural network that perfectly recognises roses and only roses.
> The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications.
I think we differ in how we see the formal methods. IMHO they are not supposed to give you 100% guarantees, because you can always cast doubt over your assumptions. Rather, I think they're a practical tool that give you a better guarantee; so in this context, a paint program verified using NN's definition of a rose is better than one that has been verified only on couple examples of a rose.
Another way to look at it - there is Curry-Howard isomorphism which states that (idealized) execution of a computer program is the same as doing logical inference, i.e. proving a formal statement. So if you're calculating 2+2, you're effectively proving that 2+2=4.
This means all software testing is a special case of a formal method. For example, when you run the test suite of your program with a new Java runtime, you are proving a statement, on these inputs my program will give the expected output, assuming we run with the new runtime. So the new runtime becomes the assumption (about the environment program runs in).
My point is, people already use formal methods, they just don't call them that. It's natural then to ask, instead of testing on a few input examples, can we instead verify a larger set of inputs (defined intensionally not extensionally)? And that's how you come from a few examples of a rose picture (extensional definition) to a definition given by an NN (intensional definition), which encompasses too-many-to-count rose pictures.
The NN doesn't have to be perfect. So what, you verified in your paint program one can also paint some pictures of not-quite-roses. Who cares? It's better verified overall.