Note, the origins are stated in Wikipedia:

> Many papers and textbooks refer the definition and proof of undecidability of the halting problem to Turing's 1936 paper. However, this is not correct.[19][24] Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.[25] A search of the academic literature from 1936 to 1958 showed that the first published material using the term “halting problem” was Rogers (1957). However, Rogers says he had a draft of Davis (1958) available to him,[19] and Martin Davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics",[26] so the terminology must be attributed to Davis.[ https://en.wikipedia.org/wiki/Halting_problem#Origin_of_the_...

The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that:

> We would note that Kleene seems, however, to have already had the self-referential argument earlier in his classic book from 1952, Introduction to Metamathematics

They also bring up the "symbol-printing problem" present in Turing's 1936 paper, which is trivially equivalent to the halting problem with today's hindsight. That paper has a well nuanced take with a lot of interesting information.

Isn’t the channel variable declared and inferred as an int32? Can’t see why the overload isn’t resolved directly?

The problem isn’t that the type inference can’t figure out that it’s a number (it can). Subtyping makes inference difficult. There may be a function somewhere which takes arguments that could be made to accept a string and an int32 (or whatever other number type that literal could be).

One thing that crossed my mind when I was looking at the TypeScript compiler. Was that it was parsing header "d.ts" files even though it wasn't used in source. Although, it had some references of a type in a small main function.

Iirc, I think this was how most compilers did. The downside is that transitive deps can easily explode. Thus, compiling a super small main function can takes seconds.

I did suggest a solution to just lazily parse/check symbols if they are encountered in source. Instead of when including a type, you have to parse all the transitive header files of the file that defines the type.

I think in the class world this is normally done by writing a service and injecting it on the constructor of the parent class. Since, React doesn't have DI built-in, it becomes problematic with the injection. hooks are essentially classes imo.

How does it become problematic? You just pass in dependencies as arguments to functions or components.

You cannot use unit tests for everything, since the number of unit tests required is basically infinity. Logically, unit tests can only prove an error exists and cannot show the program is correct. What they most likely did was mathematically showed that all possible edge cases (potentially inifinitely many) are all considered.

I have never heard of verified compiler before. Not entirely sure if I understand everything from their docs either. But here are my thoughts.

Even though you cannot unit test everything. I would still prefer it, then to have another compiler pass to ensure C semantics are the same as the compiled code. Even though compiled code is the same as C. C code can be buggy from the start.

I don't understand the use of "mathematically proven" in this context as well. Proving that x86 add instruction or a set of x86 instruction has the same as the semantics of the C code, is just pure computer science problem, not mathematic?

I fully agree. One other good point with paid software is that is more long term. It will be supported as long as there is money involved.

Just look at the JS ecosystem. Everything is for free. But also shitloads of crap. A lot of libraries left unmaintained.

Take my argument with a grain of salt. I'm not an expert. But, if nothing helped you. I can give you my experience.

What really helped me. I went from grinding a lot to almost nothing. Was, I fixed my teeth. My front teeth was a bit worn out from acid drinking and food taking. Though, they looked quite normal. My problem was that my teeth where porous. Acid always slipped into to the pores, which cause my teeths to hurt(more like itching, think like a small scratch whom). Not even brushing my teeths or washing them with listerin helped, because the acid slipped very deep into the pores. Dentists couldn't see from any xray scan what was wrong, so they refused to give me any treatment that would remove some parts of the teeth. It took me a lot of effort to convince a dentist to get me something that almost resembles a teeth crown(it was more like a filling). After getting these teeth crowns, me and my wife have not noticed any teeth grinding since.

I'm beginning to suspect whether bruxism is caused by the body's reflex to tooth ache? Note, I have amateur researched this topic a lot and I don't quite bought the argument of stress, but I was pretty convinced about the argument of the body's reaction to insufficient oxygen. But, I didn't quite bought this argument either. Because, if we worn out our teeth, it would be naturally deselected by Darwin's law a long time ago. Since, we would have a small deficiency of chewing. And it would be strange if only humans did tooth grinding and not other animals? But, what we humans have been doing a bit more recently is having an increased acid consumption, which lead to my argument if bruxism is just a reflex to tooth ache?

Note, there are treatment like (epoxy??) that can fill the pores, though it didn't helped with my ache. Once, the tooth ache was gone, so was my teeth grinding.

Basically, doing this now. I tried to implement x25519 in a highly optimized way in cpp/c and I’m in my 8 month. I dogged through countless of articles and learned a ton of abstract algebra. Though, I still feel like a beginner in this field.

I’ve done a few hard projects in my career (compilers, and graphic editor). And I think implementing a elliptic curve in a optimized way, without a math library, must be one of the hardest thing in programming.