> 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_...
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.
A thing can be explained with its constituent parts or explained by a parallel analogy. If you don't understand the constituent parts or the analogy or there are neither of these. You won't understand it.
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.
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?
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.
For easier chips like TPMs(Trusted Platform Module). What I've seen people do when trying to steal secrets(key) on a chip is to buy multiples of the same chip. On each chip expose the layer under a microscope(A chip exist of multiple layers, thats why we need multiple chips). Now, you know everything to reverse engineer the secrets. There exists tools for drilling and probing each trace on the chip. Here is an example.
https://www.youtube.com/watch?v=h-hohCfo4LA
I think what you mean by charging a huge capacitor and blowing up the secrets. You refer to an HSM(Hardware Security Module). They typically have sensors to detect any fraudulent behavior. They are much harder hack. But there is always holes in each HSM. I think hackers use the same technic there as well. Buy multiple HSM to figure out the design. Reverse engineer the traces and try to probe without being detected on the target device. To my knowledge there are currently no sensors that are 100% bullet proof. They can either be fooled or have weak spots.
I also did some review of many EDA tools. Sadly, KiCad is absolutely the worst I've tried in terms of UX. I guess many's favorites are Altium Designer. I just hope there is one Open Source solution that is similar to Alitum Designer. What they charge is restricting innovation from happening.
I think the future of back-end development is heavily decided by the future programming language. I think we are still missing a programming language that is safe, fast and productive. Safe meaning type safe and memory safe(Also memory leak safe), Fast meaning near zero abstraction costs, and productive meaning productive syntax and good tooling support. And it has to be built on modern compiler architecture, which means a compiler exposes an API for tooling(symbol lookup, refactoring, etc.), so people around the world don't need to reinvent the wheel.
I personally don't think any programming language fits the above description. And we have yet to invent it.
> 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_...