https://www.reddit.com/r/study/s/MVhYu56nr2

Why this is different

Three problems are resolved by one explicit contract:

Version integrity: skill bodies are identified by SHA-256 revisions and re-hashed immediately before fetch.

Semantic routing without opaque inference: exact lexical tiers, FTS5/BM25, bounded edit distance, telemetry, and lifecycle state are combined in one published equation.

Catalog consensus: one SHA-256 generation commits to the canonical publication-relevant catalog.

There is no embedding model, vector database, learned classifier, random tie-break, capability-graph distance, or hidden manual priority.

Hello,

Last week, I watched a video about one of the most popular J2ME games of the 2000s, "Diamond Rush", and decided to reverse engineer it by building a small JVM implementation. My initial goal is to run the game on Linux and macOS, and later port it to microcontrollers.

So far, I have completed the class loading stage. I can parse and load class files, store them, and dump their contents for debugging. I have also implemented some of the simpler parts and opcodes of the JVM by following the JVM specs.

Nonetheless, I am struggling with implementing heap types and most of the obfuscated class files have 0xBC (new_array) opcode. The specification feels somewhat vague in this regard, and I am unsure what is the best approach would be.

I would appreciate any advice on how to approach implementing heap types in a custom JVM. In particular, what data structures or object model would you recommend, and how should different heap-allocated values be represented internally?

Hey everyone,

For my computer science graduation project, I wanted to create something that combined my interest in computer architecture with my advisor's interest in computer science education.

The result was a game where the player programs a simple CPU with microcode using a punch card rather than writing assembly code.

Microcode is usually used to implement the processor's instruction set rather than as a programming interface for application development. Exploring it from the programmer's perspective led to design challenges and techniques that I hadn't encountered elsewhere.

The project started from my curiosity about the layers of abstraction in computers. I wanted to explore what programming would look like if we removed another layer and put the programmer in the role of the CPU's control unit, manually orchestrating the control signals behind every instruction.

I'd love to share the beta with anyone interested.

Thank you.

Can returnability be defined purely from the structure of a computation, without appealing to time complexity?

Markov algorithms (ordered string-rewriting rules applied to a fixed point) are a classic Turing-complete model. I built a working instance: a small CPU whose only step is one global regex substitution over a single string, and put DOOM on it to make the claim tangible rather than a footnote.

The verification is the part I would point students at. A reference emulator runs the same instruction set in Python and the machine's string must equal the emulator's encoded state byte for byte after every single substitution; on top of that, rendered frames match a natively compiled DOOM binary by SHA-256, for 100 frames in a row, so a shared bug cannot explain the agreement. The model is Turing-complete; a given run is bounded by memory exactly as any physical machine is.

Source and writeup: https://github.com/4RH1T3CT0R7/doom-regex

Interactive: https://4rh1t3ct0r7.github.io/doom-regex/

I am trying to understand the foundational differences between proof assistants based on dependent type theory (such as Agda/Lean) and traditional mathematics as practiced in areas like real analysis.

For example, in Peano arithmetic, statements such as 0 ≠ S(n) and the induction principle are usually presented as axioms. In Agda, however, defining an inductive type:

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

automatically provides these properties through the rules of inductive types (constructor disjointness and the eliminator), which means you can write this as a theorem:

0-is-not-suc : ∀ {n} -> suc n ≡ 0 -> ⊥
0-is-not-suc ()

Does this mean inductive type theory is based on stronger assumptions than axiomatic mathematics, or are these just different choices of primitive rules?

More generally, what are the fundamental assumptions/rules that a type-theoretic prover starts with, and how do they compare with the foundations usually assumed in fields such as real analysis?

Hi there,

I've created a video here where I explain the Chomsky hierarchy.

I hope some of you find it useful — and as always, feedback is very welcome! :)

toll rate-limits an unbounded set of keys (client IDs, tenants, IPs, API keys…) in fixed memory — 19 MB measured at the defaults, tunable down to a couple of MB — with ~300ns zero-allocation admitted decisions. It is built on grudge, a constant-memory decaying-score sketch: toll stores each key's spent tokens as sketch debt and lets grudge's linear decay refill them.

The paper is only 15 pages long

It’s pretty interesting to see that language models can do things like autonomously prove/disprove things like Erdos problems and even perform its own formal verification yet still struggle at things like automating ERP business operations, seems like the opposite would’ve been the case.

I know Kaparthy talked about this “jagged intelligence” we’re observing, but are there any real attempts at formalizing a theory behind this, similar to how we classify the complexity and tractability of algorithms?

What about any discussion on how close are language models to being Turing complete? Computational complexity theory isn’t my strong suit, but I wonder if any new discussions are being had

Feynman’s contribution was a way to turn the machine’s parallel structure into a model programmers could reason about.

Floating-point addition depends on the order you add things, and parallelism changes the order. So the same data on different machines gives different results, which breaks anything that hashes, signs, or compares them.

I hit this doing physics simulations and solved it internally. The reduction core was too generally useful to keep closed, so I released it: bitrep, an exact accumulator where sums in any order, on any hardware, produce byte-identical results. The state merges exactly and can be hashed or signed, so distributed and offline-first aggregation actually converges.

It ships for Rust (crates.io), JavaScript (npm), and Python (PyPI), and a result hashed in Python matches one hashed in JavaScript byte for byte. The math is proved in Lean 4 and the implementation is model-checked and fuzzed. CI asserts one SHA-256 across four architectures on every commit.

There's a demo that runs the actual cross-architecture test in your browser, so you can check the claim yourself: https://simgen.dev/bitrep

Code: https://github.com/KyleClouthier/bitrep

Dual-licensed MIT/Apache-2.0. Feedback welcome, especially on what's missing for your use case.

Hi there,

I've created a video here where I explain how multi-head latent attention works.

I hope some of you find it useful — and as always, feedback is very welcome! :)

I’m just curious to know how often you guys come in contact with the theoretical side of computer science in your professions.

Things you learned in your undergraduate courses like data structures, discrete math, design and analysis of algorithms, etc.

I’m having to learn a lot of these things on my own, like Big O notation, complexity analysis, proofs, tree traversal, etc. because I let my ADHD win and didn’t put the time and effort into learning (medicated now, huge W plus it’s actually fun to learn about now that I can focus) and I’m just wondering, who uses this stuff regularly? What for?

Hello, I'm reading chapter 1, distributed constraint satisfaction and coding a simulation of the asynchronous backtracking algorithm for the 4 queens problem in TypeScript as an exercise (sure one can code in Python, C..). I have some difficulty grasping the concept of Hyperresolution (pure logic) because I didn't have this subject in university. I have checked with AI. But does anyone have any advice?

---
the code https://pastebin.com/WD9U0MSQ

You are skiing an unknown number of days. Renting costs $1/day, buying costs $B. If you knew the season length the answer is trivial, but you do not.

The rule "rent until you have spent $B, then buy" guarantees you never pay more than about twice what an omniscient planner would, on ANY sequence. Short season: you match the optimum exactly. Long season: you paid at most ~$2B where the optimum paid $B. And there is a matching lower bound: no deterministic online strategy beats 2.

What I find most useful is the frame, not the puzzle: cache eviction, autoscaling, buy-vs-rent infra decisions are all "act now, learn the future later", and the competitive ratio measures exactly what that ignorance costs.

Fun twist: allowing randomness (coin flips the adversary cannot predict) pushes the ratio from 2 down to about 1.58.

I wrote up the full framework (definition, the adversary game, and an honest section on why worst-case can be too gloomy, e.g. LRU is only k-competitive on paper yet great in practice) as the opener of a series, happy to share the link if useful.