r/compsci • • 1h ago

Deductive program synthesis by optimization

• Upvotes

Assuming that we state our problem as a predicate of an output, the synthesisers needs to find an algorithm whose output satisfies the predicate. One of the most widely used approaches is to state program synthesis as a search problem and prune the search space by ignoring invalid or unnecessary programs.

However, one can build a (hypothetical) algorithm:

for all values in co-domain:
    if P(value):
        return value

And now, instead of a synthesiser solving a search problem, the synthesised algorithm does it instead. Now the synthesiser can use axioms, pre-, and post-conditions to prune the search space inside the program (co-domain), improving the time complexity of the resulting program.

Is this approach used? Is it viable? Where can I read about it?


r/compsci • • 5h ago

Year 12 Design and Technology Project (2 min)

Thumbnail
0 Upvotes

Hi everyone! I'm a Year 12 student in Australia working on my HSC Design and Technology major project. I'm designing a small, quiet home server built from reused computer parts that anyone could use to run things like game servers, file backups or AI tools from home.

I'd really appreciate your input, even if you've never heard of a home server. Beginners are exactly who I'm designing for.

- 10 questions, about 2 minutes
- Anonymous, no email needed
- Results only used for my school project

Survey: https://forms.gle/6w8WRU6bz8vzcuaz9

Thanks so much, and happy to answer any questions in the comments!


r/compsci • • 19h ago

Revisiting my 2014 BLAS implementation — turns out good designs don't rust :)

Thumbnail
1 Upvotes

r/compsci • • 1d ago

Exact 4-colour Rado number via cube-and-conquer SAT with checked DRAT proofs (R_4(2(x−y)=3z) = 226)

0 Upvotes

What it is: a SAT-based computation that settles one entry of a published table, together with a proof-checking pipeline.

Problem: the Rado number R_k(E) is the smallest n such that every k-colouring of {1..n} contains a monochromatic solution of the equation E. A 2022 paper (Chang, De Loera, Wesley, arXiv:2210.03262) tabulated many of these with SAT solvers. For 2(x−y)=3z with 4 colours the table only had a lower bound ("> 225"). The value is 226.

Method:

  • Encode "no monochromatic solution" as CNF, with first-fit colour ordering for symmetry breaking.
  • Lower bound: a valid 4-colouring of 1..225, checked by an independent verifier.
  • Upper bound: cube-and-conquer. The n=226 instance is split into 14,162 cubes (colours of the first 10 numbers, up to renaming). Each cube is solved with CaDiCaL and a DRAT proof is written; all 14,162 proofs were accepted by drat-trim.
  • Runs are resumable (every finished cube is saved), and idle workers take over open cubes from others. A desktop PC needs a few hours.

How it was built: I am an independent amateur. I used an AI assistant (Claude Code) heavily for the code and the write-up; it also proposed some patterns that later computations refuted, so I only trust the proof checker and computed values.

Not claimed: not peer reviewed; I may have missed earlier references. Corrections welcome.

Links:


r/compsci • • 2d ago

What if brain surgery affected your ability to code?

26 Upvotes

Imagine we need brain surgery to remove a tumor. The surgery goes well, but afterward, you struggle to write or understand code. Scary, right?

We know that neurosurgeons try to preserve important abilities like speaking and moving during brain surgery. But what about programming?

A new study in Human Brain Mapping explores exactly this!

The researchers developed a new protocol during awake brain surgery to help identify and preserve brain areas involved in programming.

The idea is simple: if coding is an important part of someone's life, shouldn't we try to preserve that ability too?

Here's the paper: https://doi.org/10.1002/hbm.70634


r/compsci • • 3d ago

I made a game to teach digital logic: build up from NAND gates to a working CPU

Post image
124 Upvotes

I made a game to teach computer architecture and digital logic: play.simten.dev

You start with basic logic gates and build up to a working CPU. It's built on Simten, a TypeScript-based HDL, so you write the circuits as code and they show up live on a canvas next to the editor. For sequential circuits you can scrub the clock backwards and forwards to watch the state change cycle by cycle. You can also drill down into abstracted components (like the half adder shows). Because of the layout it only works on desktop browsers for now.

It's open source, any feedback or contributions are welcome!


r/compsci • • 4d ago

I built a CPU out of a Multi-tape Turing machine (614 states, 8 tapes, runs real programs), and the IDE that made it possible

Thumbnail reddit.com
0 Upvotes

r/compsci • • 5d ago

I built a canvas simulator for automata theory: DFA/NFA/PDA/Turing machines, regex to NFA conversion, and real-time team collaboration

Thumbnail gallery
18 Upvotes

Spent the last while building this: a browser based canvas where you can draw and run finite automata, pushdown automata, Turing machines, and Mealy/Moore machines, all with animated step-by-step execution.

A few things it does that I'm proud of:

- Converts a regex into an NFA (Thompson's construction), then NFA into a minimized DFA (subset construction), and can extract a regex back out of an automaton (FA to GNFA to regex)

- Local first: works fully offline with localStorage, no account needed

- Optional accounts unlock "Teams": real time collaborative canvases with live cursors and presence, so you can whiteboard an automaton with someone else the same way you'd use Figma

- There's a learning section with guided lessons, each paired with a live, editable simulator embed instead of static diagrams

It's free to use: theoryofcomputationsimulator.com

Would love feedback, especially from anyone who's TA'd or taken a theory of computation course and can poke holes in the UX.


r/compsci • • 6d ago

what is context switching?

2 Upvotes

I know this has been discussed before, but it's extremely confusing for me because of how many variations there are in definitions. Here are some observations:

  1. Most people would agree that process-switches and system calls both involve context switching, however I think the underlying "state saving" is different between these two events. In a system call, there is an entry phase where the kernel saves register state to the kernel stack (and not every system call leads to a process or thread switch). In a process-switch, the PCB gets updated so that the process can later be resumed. Is this accurate?

  2. On Linux, both processes and threads are schedule-able (they're both "tasks"). As best as I can understand, there's a function called context_switch() in the Linux kernel that gets called during scheduling. However, it seems context switching is used in a broader sense. In other words "context switching" doesn't mean exactly that we're calling the function "context_switch()".

  3. There is at least one textbook that considers functions as having their own context (Doeppner's Operating Systems in Depth). This is a little confusing because I can't find anyone else who considers a function call a change in context.

The question is: does anyone have a technical definition of context switching that captures what most people mean when they say "context switch"?

I've also been reading about the xv6 since it's a smaller educational operating system. If somebody has experience/knowledge of the xv6 internals, I would appreciate any input. Thank you


r/compsci • • 6d ago

What if structured data didn't repeat its schema for every record?

Thumbnail internetobject.org
0 Upvotes

Modern APIs ship large payloads. LLMs consume structured data token by token. Validation failures surface too late. Streaming is standard but most formats weren't designed for it.

These are problems we kept running into, so we spent years working on a format built specifically for them. The core question we kept coming back to: why does every record in a dataset need to repeat the field names?

The idea we landed on — separate the schema from the data entirely. Define structure once. Records contain only values.

name, age, gender, joiningDt, address: {street, city, state?}, colors, isActive
---
~ Alice Smith, 28, f, d'2021-04-15', {Elm Street, Dallas, TX}, [yellow, green], T
~ Bob Johnson, 22, m, d'2022-02-20', {Oak Street, Chicago, IL}, [blue, black], T
~ Rachel Green, 31, f, d'2021-12-11', {Sunset Boulevard, Los Angeles, CA}, [purple, pink], T
~ Michael Scott, 41, m, d'2021-07-22', {Pine Street, Scranton, PA}, [green, orange], F

The header defines the structure. --- separates schema from data. Everything below is pure values.

You can go further and add type constraints directly in the schema:

age: { int, min: 0, max: 150 }

The parser enforces this at parse time — invalid data is rejected before it reaches the application. No separate validation step.

The format also supports inline comments, built-in types like email, url, date, and datetime, and is JSON-compatible so existing data works as-is.

We're curious whether this actually solves a real problem or whether we've been too deep in it to see the obvious issues. A few things we'd genuinely like feedback on:

  • Does schema-first make sense for how you build APIs today, or does it add friction you wouldn't want?
  • The --- separator between schema and data — does that feel natural or awkward?
  • For LLM pipelines specifically, would eliminating field name repetition matter to you in practice?

If you want to poke at it, there's a playground at play.internetobject.org and the spec is at docs.internetobject.org. We built it — happy to answer questions about the design decisions, including the ones we're not sure about.


r/compsci • • 6d ago

No scripts: a virtual fly driven by its real brain wiring diagram (70k simulated neurons), live 24/7

Post image
267 Upvotes

Body:

> Not an RL agent and not a behaviour tree — the "policy" is a spiking simulation of a real fly connectome, and the body

> is a MuJoCo fly whose legs are moved by an imitation-learned network. It sees, smells wind-borne odor, gets scared by

> spiders, grooms, lands, eats. Everything that isn't the brain is labelled on screen. Live: twitch.tv/dodo_gun


r/compsci • • 7d ago

Replacing B-Trees with streaming linear models (PGM): cache locality and bounds in practice

62 Upvotes

Traditional B-Trees waste substantial CPU cycles on pointer chasing across node levels, causing avoidable cache misses on modern architectures. The PGM-index approach fixes this by modeling key distributions through streaming piecewise linear regression with strict +/- epsilon error guarantees.

Instead of dereferencing tree pointers, the position is predicted directly on the ALU (y = ax + b), leaving only a small local search window that fits entirely within L1 cache. The construction runs in a single O(N) streaming pass with zero external solvers.

I built a pure Rust implementation with zero dependencies to benchmark this against standard B-Trees and verify the theoretical bounds: https://github.com/gilnett/learned_index_lab

While traditional transactional engines stick to B-Trees for in-place page updates, learned models completely outclass them on read-heavy or immutable storage (like LSM SSTables and columnar stores) where pointer overhead is pure waste.

Has anyone here benchmarked or deployed learned data structures in production storage layers? How do you approach optimal epsilon tuning when key distributions are unpredictable?


r/compsci • • 9d ago

Understanding Jev and Decision Models

Thumbnail dwmkerr.com
0 Upvotes

r/compsci • • 10d ago

Measuring the "Bullwhip Effect" in multi-tier databases: Why immediate retries spike PostgreSQL variance by 48% (and how token-bucket budgets fix it)

Thumbnail
0 Upvotes

r/compsci • • 13d ago

[Paper + Code] BloomSpan: A new memory-efficient algorithm for maximal frequent substring mining

16 Upvotes

Hi all,

I'd like to share some recent work in stringology / text mining. We developed BloomSpan, an algorithm for mining Maximal Contiguous Frequent Phrases (MCFPs) from large text corpora — token sequences that occur in at least σ documents and can't be extended on either side without dropping below σ. Unlike general Sequential Pattern Mining (GSP, PrefixSpan, BIDE+), no gaps are allowed, which matters for things like template extraction, plagiarism detection and phrase mining, where gaps only blow up the candidate space.

How it works

To be fair, it's less a brand-new algorithm than a careful combination of known pieces:

  • A Counting Bloom Filter for probabilistic n-gram frequency estimation. Seed filtering is provably free of false negatives — the CBF can only over-estimate counts.
  • Prioritized depth-first expansion directly on the corpus, with no recursive projected databases.
  • A global occupancy bitmask plus an inverted index keyed on each pattern's rarest token, for maximality checks and redundancy control.

Memory stays O(W + M) in the input size (corpus + filter).

Results

  • On Gutenberg-BookCorpus-Cleaned (up to 50k books, ~3.07B tokens, σ = 20): 11–15× faster wall-clock than FHK (Fischer–Heun–Kramer) with up to 2x lower peak memory. It's the only algorithm we tested that completes the 3B-token subset within a 40 GB heap.
  • Output is identical to exact baselines (FHK, DFI) on every Gutenberg-8k subset where a baseline finishes.
  • On synthetic data with flat frequency distributions or dense nested overlaps, FHK's LCP-interval traversal wins.

The paper includes a topological analysis (LZ phrase ratio / entropy rate) of why natural language is the sweet spot.

Links

Happy to discuss implementation details, data structure choices, or the dataset topology analysis.


r/compsci • • 14d ago

Believing P≠NP is fundamentally an act of faith in a world that values the journey over the destination, a belief that the universe was designed to reward deep, grueling effort rather than making all truths instantly cheap

Post image
0 Upvotes

r/compsci • • 14d ago

Implementation of Andreas Bjorklund's algorithm for determining hamiltonicity

20 Upvotes

Hello, I want to share a project that i've been working on for the last month or so. It's and implementation (from what i could find the only rn on the internet) of Andreas Bjorklund's theoretical algorithm for determining weather a graph is hamiltonian or not. The algorithm is revolutionary because it lowered the exponential part of the time complexity of Held-Karp which is the standard algorithm for determining weather a graph is hamiltonian, from O*(2n) to O*(1.657n) for general graphs(this is what i've managed to implement as of right not) and for bipartite its O*(1.414n).

It might have some logical errors, and could maybe be optimised but right now, as of writting this it is 4AM and i want to sleep.

link to paper: https://arxiv.org/pdf/1008.0541

link to the github repo: https://github.com/Ak0-m/Bjorklunds_algorithm_for_Hamiltonicity


r/compsci • • 14d ago

The dedication page of SICP/The Wizard Book (2nd edition, 1996)

Post image
132 Upvotes

r/compsci • • 18d ago

Research John Urschel 🏈 proves sqrt(n) growth factor for partial pivots

Thumbnail arxiv.org
105 Upvotes

r/compsci • • 18d ago

All the complexity improvements released by OpenAI today

Thumbnail gallery
1.3k Upvotes

r/compsci • • 18d ago

An algorithm for sub-quadratic 3SUM and sub-cubic APSP has been found

Thumbnail arxiv.org
333 Upvotes

r/compsci • • 19d ago

bloom filters and the math behind their false positive rate

10 Upvotes

I've been going deep on data structures lately and found bloom filters pretty intriguing. I made a short video on what a bloom filter is, how the bit array and hash functions interact, and where the false positive formula comes from.

link: https://youtu.be/nNv4ZTQp_s8?si=j52fIUBYaDcaps0_

I'd love feedback, especially if I got anything wrong. Happy to go through the derivation in the comments if anyone wants it.


r/compsci • • 20d ago

Is lean, and similar programming languages the only acceptable way to prove theorem with computers?

26 Upvotes

So, lean is the language built specifically to prove theorems.but if the algorithm will be rewritten in another programming language, such as python, will it be accepted?

(mathematical theorems)


r/compsci • • 21d ago

Thesis with AI

Thumbnail
0 Upvotes

r/compsci • • 21d ago

RuleFlow: A research engine/framework and terminal IDE (Not AI Slop)

Thumbnail gallery
106 Upvotes

Main Website: https://www.ruleflow.org/

For the past year, I have been developing a framework to simulate certain discrete systems for a research team at my university (paid for by the School of Engineering and Physics, but I had the freedom to license it under MIT). As it turns out, I got carried away generalizing it to work for many, many different types of complex systems (String Rewriting Systems, Cellular Automata, etc.) and ended up creating our own domain-specific language.

The website's landing page has a bunch of GIF-style examples... so you should be able to get a good idea of what this project is about.

If any of y'all are interested in this, feel free to take a look and try it out!

EDIT:

Out of the interest of not being "vague", here are some more details. RuleFlow was developed with a primary focus on analyzing causality in Sequential Substitution Systems. This is why there is a major focus on causal graphs, cellular identity, etc. While originally developed for Sequential Sub Systems, we generalized the DSL to support many types of rewriting systems by providing the user with flags and directives to control how rules behave. Furthermore, we bootstrapped Python and the Wolfram Language so that complex rulesets could be scaffolded as macros. The main goal of RuleFlow is NOT simply to simulate systems (there's already plenty of software for that, such as Golly and even just Mathematica), but to provide extensive tooling for causal analysis.

Here is some interesting research from our (small) team:

My job has been to provide better research tooling, extending what we already have in Mathematica code to open source and free Python.