That chart implies it is possible for somebody to write a work that wins the Hugo awards for best novelette and best novella, which I’d really like to see happen!
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.
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".
99% of the time the answer is speed. It's just way faster to evaluate and build all of this at compile time than at runtime.
I understand both sides of the argument here - on one hand you have fast and unreadable code and on the other hand slower and more readable code. The problem here is 1. the leaky abstraction of characters and code points and 2. loss of type safety due to C's weak typing rules, which is a bit lost in the "hurr durr messy code."
Since you can pass types to compile-time functions, yes that is correct. Take the example [from the 0.6.0 documentation](https://ziglang.org/documentation/0.6.0/#comptime) for example: At compile time the compiler has to figure out whether to type the `max` function using `u32` or `f64`. Since you can make the boolean condition arbitrarily complex the _type_ of max function called is undecidable in general.
I'm not arguing for or against undecidability in type systems, the page aims to be present the information neutrally.