tristenharr

I'm still working on Logos Language. Just launched v0.10.0 :)

https://logicaffeine.com/benchmarks

This is the silliest take I’ve ever read. Strong type systems are an AI’s best friend.

Feels related to research I've been doing with Author2Vec! https://author2vec.com/

I truly believe that now with all the post-training these AI models know some of us not just as fuzzy vectors but as individuals with a specific location within the Jacobian workspace that they tend to work from.

This thesis is why I keep separate Claude accounts, some for letting them train on my data, and another for work that must stay private. The more that it seems Claude will come to know you based on your fingerprint defined by your word choices and the fingerprint making up basically a mathematical representation of the way your brain is wired to do language.

If you want a model to do good work I hypothesize it is better to make sure that your project has a representation to work from within it's jacobian workspace!

Yes that's the language, the v0.10.0 benchmarks are coming very soon and with it some major updates. We've added supercompilation and symmetry breaking to the optimizer pipeline. Sneak peeks available on a branch currently named stream1. https://github.com/Brahmastra-Labs/logicaffeine/tree/stream1

I wanted to major in Philosophy but was worried I wouldn’t make enough money to support the lifestyle I wanted so majored in Computer Science instead. What irony.

Someday I hope to go back to school to get a PhD in philosophy with a focus on logic. :)

I’ve been shocked by how much LLVM leaves on the table while designing Logos language! Some very exciting benchmarks coming soon that we’ve been working on for over 6 months, but LLVM misses a LOT of potential optimizations when you have a strong type system!

Lately I’ve felt Kolmogorov complexity is an unfair measurement because it takes for granted your underlying programming language as treats it as zero cost. In theory you could create a custom language and embed the program as data and “compress” a large random sequence with a better Kolmogorov complexity for that specific language than Pi, simply by not exposing the ability in the language to even work with Pi. I think what’s maybe more interesting is when you take into account the work of Dr. Futamura and the idea of Jones Optimality and view things through that lens.

Hey all, I didn't actually use Claude for the embeddings on this (bc they don't offer embeddings), but I think we can extrapolate that if a tiny open source model has this level of recognition, surely the SOTA models do. Very interesting to me that we can predict things like gender and college from a sample of writing for authors. Also interesting how much stronger the correlation may be between Coders and their Code to authors and their books. Seems code has a more "unique" fingerprint than your typical book perhaps. (Although actually looking at it again perhaps that's sample size. Would need to research more to know for sure.)

Author recognition seems to climb as a smooth gradient with author exposure in LLM's. :)

Thinking about this as I continue working on Logos language prepping for our 0.10.0 release, finished our copy-patch JIT that does hot-tiering and found myself wondering why I was going to all the trouble to native tier with a big game of compile to Logos Lang -> JIT to either my Bytecode language or Rust for compiled -> GCC -> WASM

So I'm writing a WASM JIT, and I'm wondering why things never got to that point? Is it just beyond human comprehension? (Don't get me wrong here, I would not be writing something Jitting to WASM without AI, and maybe it's these types of projects that simply weren't feasible or something to consider pre-AI unless you were very rich and very bored.)

I thought for a second you were talking about Logos Lang! The language I’m working on that we believe will be humanities last language. Best of luck, and good to have competition. How’s your FFI support? ;) https://www.logicaffeine.com/

Woah this is AWESOME! I am going to have to take a look! Love the thoughts, doing something similar at https://logicaffeine.com/studio

Check out Logos lang, would love to chat sometime. love that you chose Haskell!

3 days of refactoring, over 140,000 lines of code touched. All ~2500+ tests still passing. I'm going to sleep! Another all-nighter. Talk about a fun Friday night! :) I frickin love this stuff so much! It's like having an ARMY. A LITERAL ARMY OF PHD's. You can raise mountains in minutes it feels like. That's been my experience. You all may call it slop, but I think spec driven development is great. I just think that if you have to write documentation to explain the code, then either your language syntax isn't precise and easy enough to understand, or you are doing something convoluted and potentially stupid. It's a language surface problem. The languages of the past were constrained by human limitations. In the past you'd be out of your mind trying to write a crazy multi-pass compiler and doing all the tips and tricks to make something fast because a human had to maintain it. If you formally specify the constraints of something, design tests that codify those constraints, and then develop code that passes those tests without cheating or changing them, then these new technologies rapidly gain something that gets much closer to determinism.

I think for me the key thing has been treating the tests like I'd treat my foundation. When something is wrong, or I need to design something, it starts with a spec that tries to solve the domain problems, which turns into a plan for tests that will fail when we run them now, but should pass when we have completed the implementation. You may miss edge cases, but when you identify them, you fix them for good by adding tests for them.

One of the tricky parts is creating a good test harness. You have to have a great harness and I need to go through and improve mine!

Anyways, I'm exhausted folks, pizza is all gone and the mountain dew ran out. Time for me to snooze.

Enhancements Short Term Roadmap -> https://github.com/Brahmastra-Labs/logicaffeine/issues?q=is%...

Creates: https://crates.io/crates/logicaffeine-base https://crates.io/crates/logicaffeine-data https://crates.io/crates/logicaffeine-kernel https://crates.io/crates/logicaffeine-lexicon https://crates.io/crates/logicaffeine-system https://crates.io/crates/logicaffeine-proof https://crates.io/crates/logicaffeine-language https://crates.io/crates/logicaffeine-compile https://crates.io/crates/logicaffeine-cli

Documentation: https://docs.logicaffeine.com Studio Example: https://logicaffeine.com/studio?file=examples/code/memory/zo...

Really enjoyed reading this. Stuff like this is what inspires me to keep pursuing logos language and theorem prover. Things on the roadmap next include stuff like adding first-class inline ASM support. Adding great SPMD and auto-vectorization pipelines, and exploring making verifiable private computation a language primitive when you make things private. If interested, read about some of the planned upcoming enhancements here. :) https://github.com/Brahmastra-Labs/logicaffeine/issues

Hey folks, some more fun things have come to Logos Lang, including an initial cut of the theorem prover using CoC.

Please excuse the mobile formatting on the studio page, fixes coming to that soon, for best experience check it out on the web!

Yes, absolutely! I definitely want to look into this, although it's not the top of the current roadmap.

To me, the first step is going to be to really work through and trying to get this right. Do user studies. Watch people write code in this. Watch people with lots of experience, and people with none get tossed into a project written in the LOGOS and told nothing.

Once the language surface is more solid and not as likely to go through major changes, I want to focus our efforts in that direction.

Crates coming soon! :)

Hello, author here! The license is BSL 1.1 based on the MariaDB license, the source transitions to MIT on December 24th 2029. We're a small bootstrapped team, and I was worried if I went full on FOSS from the get-go a big player might resell it with a easy one click button to deploy things like the playground and such that's coming soon and I'd struggle to feed myself while maintaining a potentially growing project while others reaped the fruits of the labor. I've seen that kind of thing happen a lot in recent years. I also am aware somebody could code-launder things, but personally I'd take that as a compliment, if somebody truly wants to copy my programming language and such, then I'd be glad to have inspired someone haha! We're tiny, bootstrapped, and nobody has ever heard of us so that kind of attention alone would be awesome!

It's free for individuals, orgs with < 25 people, educators, students, and non-profits, and I'm currently still working through monetization but I'm thinking of taking two paths, one being payment to get the Z3 verification feature that lets you mathematically verify that the code won't panic at runtime. The other being payment to use the tokenizer that will be built with this. If you look here you can see the lexicon to get a better idea how the english compile pipeline works. https://github.com/Brahmastra-Labs/logicaffeine/blob/main/as...

This also makes the language highly configurable as you can change any of the key-words to better suit your brain if you so chose.

Current LLM's biggest bottlenecks in my personal opinion would be the tokenizers and the way they get their info. Imagine if you got fed in random chunks of tokens the way they do. If you could create an AST of the english and use that to tokenize things instead... well at least I have some hair-brained theories here I want to test out. Standard LLM tokenizers are statistical and they chop words into chunks based on frequency, often breaking semantic units. This lexer could perform morphological normalization on the fly, an LLM spends millions of parameters to learn that the word "The" usually precedes a noun, but this parser knows that deterministically. This could be used to break things into clauses rather than arbitrary windows. Even just as a tool for compaction and goal tracking and rule following this could be super useful is my theory. A semantic tokenizer could potentially feed an LLM all parse trees to teach it ambiguity.

There is a test suite of over 1500 passing tests. I do utilize Claude, but I try really hard to prevent it from becoming slop. Development follows a strict RED/GREEN TDD cycle, where the feature gets specced out first, the plan and spec gets refined and tests get designed, then the tests get written and then implementation occurs. It is somewhat true that I can't make as many promises about the code regarding untested behavior, but I can make promises regarding the things that have been tested. The test suite is wired directly into CI. I guess it is fair that some people will feel any code written with the assistance of an LLM is slop, but everyone is still working out their workflows and personally you can find mine here: https://github.com/Brahmastra-Labs/logicaffeine/blob/main/Tr...

TLDR of it would be: 1. Don't Vibe-Code 2. One-shot things in a loop and if you fail use git stash. 3. Spend 95% of the time cleaning the project and writing specifications, spend 5% of the time implementing. 4. Create a generate-docs.sh script that dumps your entire project into a single markdown file. 5. Summon a council of experts and have them roleplay. 6. Use the council to create a specification for the thing you are working on. 7. Iterate and refine the specification until it is pristine. 8. Only begin to code when the specification is ready. Use TDD with red/green tests.

I'm always learning though, so please if you've got suggestions on better ways share them!

That is a valid concern! To clarify:

Configurability: We absolutely plan to make the 10ms yield interval configurable (or opt-out) in the runtime settings. It is currently a default safety rail to prevent async starvation, not a hard constraint.

Concurrency Options: It is important to note that LOGOS has three distinct execution primitives, and this yield logic doesn't apply to all of them:

Simultaneously: (Parallel CPU): This compiles to rayon::join or dedicated std::threads. It does not use the cooperative yield check, allowing full blocking CPU usage on separate cores.

Attempt all: (Async Join) & Launch a task: (Green Threads): These compile to tokio async tasks. The cooperative yield is specifically here to prevent a single heavy async task from blocking the shared reactor loop.

So if you need raw, uninterrupted CPU cycles, you would use Simultaneously, and you wouldn't be forced to yield.

Oh, I'm glad this got picked up! I posted it on New Years day and wasn't sure if it was going to be!

As a bit of background on myself and my goals/targets with this.

I started my career as an embedded software developer writing uCos-III for an RTOS working on medical devices for Cardinal Health where I primarily worked on enteral feeding pumps. From there, I spent a couple years in fintech, before trying my hand at my first startup where I co-founded a company in the quick commerce space. (Think similar to Doordash Dashmarts). When that fell apart I took a job at Hasura where I wrote GraphQL to SQL transpilers and other neat things for about 18 months. I've worked across a few different domains and the motivation behind writing this language is that I am preparing to teach my 13 year old brother how to code and wanted something I could get low level with him on, without losing him altogether.

This is a dual-purpose language and has a dual-AST, and the things I'm currently working on... having switched gears towards spending a couple days on the Logical side of things are adding an actual prover to the Logical AST. I'm getting ready to add a derivation tree struct and incorporate the ability to use a solver to do things like Modus Ponens, Universal Instantiation, etc. I also want to upgrade the engine to be able to reason about numbers and recursion similar to Lean with inductive types.

This is an early access product, it is free for students, educators, non-profits, orgs with < 25 people, and individuals.

It would make my day if I could get some rigorous HN style discussions, and even the critiques!! The feedback and discussions are invaluable and will help shape the direction of this effort.

What a lovely surprise doing my daily HN check before bed and seeing this post. :)

EDIT: I will read and respond to comments when I get up in the morning, feel free to ask questions! Or make suggestions.

Happy new year HN! After a few late nights this past week, I've finally got this one over the finish line just in time to kick the year off.

I'm happy to answer any questions that might pop up...

Some things of note:

Built-in P2P Mesh Networking

Listen on "/ip4/0.0.0.0/tcp/8080". Connect to "/ip4/192.168.1.5/tcp/8080". Sync counter on "game-room".

That's all you need for libp2p, QUIC transport, mDNS discovery, GossipSub pub/sub

Full conflict-free replicated data types: - GCounter, PNCounter — distributed counters - ORSet with configurable AddWins/RemoveWins bias - RGA, YATA — sequence CRDTs for collaborative text editing - Vector clocks, dot contexts, delta CRDTs

Wrap any CRDT in Distributed<T> and get: - Automatic journaling to disk (CRC32 checksums, auto-compaction at 1000 entries) - Automatic GossipSub replication to all peers - Unified flow: Local mutation → Journal → Network. Remote update → RAM → Journal. - Survives restarts, offline nodes, network partitions.

Go-Style Concurrency - TaskHandle<T> — spawnable async tasks with abort - Pipe<T> — bounded channels (sender/receiver split) - check_preemption() — cooperative yielding every 10ms for fairness

There's more... but those are my personal favorite features.

I've put a good bit of work into this, so I hope you all can appreciate and maybe find some uses for it here on my favorite place on the interwebs!

Ah yes. I very well may be going a bit crazy.

Well whatever mental health struggles I am enduring, it is certainly Hasura’s fault. More specifically, Tanmai’s fault. But I’m sure he’ll run the company into the ground without any help needed before too long.

It’s a horrible thing man. Did you not hear the story? I was told I was getting promoted and moved onto a new team at the offsite, then when I went into my performance review expecting the promotion and suddenly I was fired. You know how things go at Hasura… everyone just disappears sooner or later.

You know how it goes… Tanmai decides he doesn’t like someone, so he just kicks them out the door, no matter how hard they work or how much it might hurt his company.

Idk man, I would get out if I were you.

I literally turned down the severance because of just how messed up what they did was, so I could speak about it publicly in places like this.

Polylogarithm values at a golden ratio based argument paper:

https://zenodo.org/records/15696357

Posted 1 week ago on Zenodo, 8k views, >900 downloads, supposedly is a lot for number theory?

I have no idea.. would love a discussion here.. do you have math friends?

Requesting help with formalization in Lean!

Here’s what I have so far:

https://zenodo.org/records/15744937

Author here! :) Would love to hear from others on this. It seems to have decent interest but I don’t know much about academia and such so maybe the amount of traffic is normal for a first paper, or perhaps it’s the bots.. it just seems like a lot of views and downloads.

I’ve found the 2.5 pro to be pretty insane at math. Having a lot of fun doing math that normally I wouldn’t be able to touch. I’ve always been good at math, but it’s one of those things where you have to do a LOT of learning to do anything. Being able to breeze through topics I don’t know with the help of AI and a good CAS + sympy and Mathematica verification lets me chew on problems I have no right to be even thinking about considering my mathematical background. (I did minor in math.. but the kinds of problems I’m chewing on are things people spend lifetimes working on. That I can even poke at the edges of them thanks to Gemini is really neat.)

from sympy import sqrt, isprime

T1 = (sqrt(5) - 1) / 4 J1 = (3 - sqrt(5)) / 4

def golden_prime_generator(limit): primes = [] for n in range(2, limit): Fn = ((T1 / J1) * n - (-J1 / T1) * n) / sqrt(5) val = int(Fn.round()) if isprime(val): primes.append(val) return primes

my_primes = golden_prime_generator(1000) print(my_primes)

2930441286939258055400798002200365702070383356835498296052929375099603314612750189999474839964041401824000060018138590135001102587299815016150326470813100791358366141506590207652108187961822226141844888227246720852693565292520772736233258137883131633884772691595926733322344165957105221939274575774318941464860860848233258397675536343685662420797069118608961212878580658178971916344998597383060635840095569469168798433682688690011514459699339511226211249166351120903825586706980141114247391189112452169301152785673208885984700944382085177499062708435697669359679050984522704457968238198039501357594162223897683190805618618838233503289429282246135842585430668875653560981464799218782095773523505176978173330569112583486848660662068908749844158638271675670908226354975956636181462553977591227553535134946781776535903879669168739541718125413163115489438127173145671369147353184448182943977584875431449095152717023151009740993170461840098542328540055499213188472025194001595310097403036158566599062407003698164302276578800844789715519909977450325416955326392430087122738870988283653737701175138504893394815816782040327194725855833