seeknotfind
One particularly famous example of a bug: https://projectzero.google/2023/01/exploiting-null-dereferen...
We usually get away with ignoring unsigned rollover because most application counts don't exceed 2**32 or 2**64. However, many can exceed these values, and in those cases, explicitly handling this case in critical systems is often better than ignoring potentially erroneous behavior.
Another concern, some people might have about this is the performance implications or what to do when you want to allow overflow. In that case you can locally disable overflow protections.
My man Terrance Tao, I hope to contribute to your symphony of progress.
If the interrelationships of this are also exposed and searchable, if it can build many bridges inside itself, then this is truly the cipher key to all that can be known.
The real technical blocker is performance and voice synthesis. If voice synthesis was at parity with human actors, it would be worth it to battle the performance aspect for major studios. In text based games especially, taking time to generate enough text is just too slow to be convenient
Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover this issue. Also, allocation counting.
Hey also sucks you are not in SF. I'm looking for people into formalization in the area, but I haven't found any yet
struct Ascii {
std::shared_ptr<Bool0::bool0> _a0;
std::shared_ptr<Bool0::bool0> _a1;
std::shared_ptr<Bool0::bool0> _a2;
std::shared_ptr<Bool0::bool0> _a3;
std::shared_ptr<Bool0::bool0> _a4;
std::shared_ptr<Bool0::bool0> _a5;
std::shared_ptr<Bool0::bool0> _a6;
std::shared_ptr<Bool0::bool0> _a7;
};
From theories/Mapping/NatIntStd.v:
- Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
consider the translation of [nat] into [big_int].
https://github.com/bloomberg/crane/wiki/Design-Principles#4-...
> Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.
What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.
Composing injective functions is like applying a permutation array to another.
However, even now, you can imagine that if quantum computers were small enough, it would be worth it to have it just for the asymptotically fast prime generation with Shor's algorithm. I don't think that's that far fetched. Of course, people wouldn't necessarily need to know they have a quantum computer, but they don't necessarily know the workings of their computers today anyway.
Say for instance that you could arrange quarks in some way, and out pops, from the fabric of the universe, a way to find the next busy beaver numbers. Well, we'd be really feeling sorry then, not least because "computable" would turn out to be a misnomer in the formalism, and we'd have to call this clever party trick "mega"-computable. We'd have discovered something that exists beyond turing machines, we'd have discovered, say, a "Turing Oracle". Then, we'd be able to "mega"-compute these constants. Another reason we'd really feel sorry is because it would break all our crypto.
However, that's different than the "idea of Chaitan's constant" existing. That is, the idea exists, but we can't compute the actual constant itself, we only have a metaphor for it.
We cannot compute exactly what happens because we don't know what it is, and there's randomness. Superdeterminism is a common cop out to this. However, when I am talking about whether something is computable, I mean whether that interaction produces a result that is more complicated than a turing complete computer can produce. If it's random, it can't be predicted. So perhaps a more precise statement would be, my default assumption is that "similar" enough realities or sequences of events can be computed, given access to randomness, where "similar" is defined by an ability to distinguish this similulation from reality by any means.
Some intuition:
1. If the universe contains an uncomputable thing, then you could utilize this to build a super turing complete computer. This would only make CS more interesting.
2. If the universe extends beyond the observable universe, and it's infinite, and on some level it exists, and there is some way that we know it all moves forward (not necessarily time, as it's uneven), but that's an infinite amount of information, which can never be stepped forward at once (so it's not computable). The paper itself touches on this, requiring time not to break down. Though it may be the case, the universe does not "step" infinitely much information.
One quick side, this paper uses a proof with model theory. I stumbled upon this subfield of mathematics a few weeks ago, and I deeply regret not learning about it during my time studying formal systems/type theory. If you're interested in CS or math, make sure you know the compactness theorem.
Paper direct:
https://jhap.du.ac.ir/article_488.html
I enjoyed some commentary here:
https://www.reddit.com/r/badmathematics/comments/1om3u47/pub...
See also:
https://en.wikipedia.org/wiki/Mathematical_universe_hypothes...
To do a new job, build afresh rather than complicate old programs by adding new "features".