Now you’ve just shifted the problem to a much harder statement: proving the things the NN recognizes as a rose is actually a rose.
You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.
Yeah. That's why I am saying it's the epistemological problem.
In the above example, that NN recognizes rose as a rose is an assumption that it is correct as a model of the (part of the) world. On that assumption, we get a formal definition of "an image of a rose in the pixelated image", and we use that to formally prove our system allows roses to be painted.
But getting rid of that assumption is I believe epistemologically impossible; you have to assume some other correspondence with reality.
I agree with you on the hardware. I think the biggest obstacle to software formal correctness is the lack of formal models of which we can be confident describe our environment. (One obstacle is the IP laws - companies do not like to share the models of things they produce.)
Right, the problem is that one can't formally describe the environment, and any one thing has to interact with it. So formallness goes right out the window.
There are even cases where it is context-depedent: Maße (measurements) and Masse (mass). Both are written MASSE uppercased, but how do you know which one's which?
For additional fun: Swiss German doesn't use ß at all, so there is no difference between "in Maßen genießen" (to enjoy in moderation) and "in Massen genießen" (to enjoy in large amounts).
Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable.
Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".
I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?
It is already bad, that we need jurisdiction for such things in the web. I think we actually need such things to happen more often, so ppl can finally vote with their fest a long time ago for some freedom against a tiny bit of convenience. I think what we lack is a decent amount of social pressure.
What we need is the largest tech companies broken into smaller pieces.
The de facto monopoly of most of these players exists in their cross-border market share, making enforcement under traditional antitrust law in any one country difficult.
Unfortunately, it's also something of an international zero sum game due to efficiences of scale -- if the US breaks up Amazon, Alibaba gains world market share, and we're back in the same place.
The most effective remedy I can think of offhand is government involvement in a special, independent branch of the company, dedicated to increasing interoperability and exposing services, empowered by legislation.
If we're going to have monopolies, at least they can be open ones. E.g. 18F + Google Takeout, backed up by regulation
Base64 is just like base10 but they needed 55 more characters beyond the 0-9. So someone decided to use letters (both lower case and upper case) and a few symbols.
You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.