Egregoros

Signal feed

API Docs
Timeline

Post

Remote status

Context

8
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun :neocat_sweat: i barely know what i'm doing with this shit half the time. i mostly talk to an LLM about it these days and it stares at me in response.

something particularly weird is how structurally neuromorphic these things are. they get there through funny routes (explicit RNG deciding when to not update = heterogenous neurons)

the fuzzy machine already makes clauses do graded activation so its straightforward enough to group them up and do winner-take-all lateral inhibition, the question is just if that pooler is useful for anything :blobcatwaitwhat:

the bizzare thing is its theoretically possible to do some kind of hopfield memory / autoregressor thing -> decider -> loop without an FPU anywhere in sight.

its a comically cheap substrate that just needs to be puzzled out in the correct order to do something smart. hm.
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun i haven't seen it, no. i've been adjacent to the proof space recently though. Maude is used for defense verification. (though i'm trying to use maude for codegen, which ran in to some stupid errors.)

there is a controversy right now, though, because openai is flooding math papers with bad proofs.
Replying to @icedquinn@blob.cat

Replies

8
Replying to @sun@shitposter.world
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun i still ultimately think model-based code, with fixed transforms, and a notebook interface, is probably the "best" form of code.

my huge annoyance with years of language cycling is that they all scuff being able to actually reuse patterns. or they make pattern reuse more expensive than it needs to be (lisp, rust, nim, zig, et all, "macros" just dump you with an AST and fuck off. they don't really help you get there faster.)

maude has the tools to try out if term rewriting is gonna work. current side note is something like an Io runtime as a kernel, and then refal-esque for the term rewriting part, though i'm tired of writing parsers and term rewriters are inherently regex machines with extra steps.

a lot of days idk what the point is. i waste time caring about things not breaking while everyone is getting paid to vibe :blobcatghost:
Replying to @icedquinn@blob.cat
Replying to @icedquinn@blob.cat
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun > https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf

oh they're doing ATS' ghost code thing. linear typed proofs. very strong if they get it right. ATS' failure was it never got a syntax that was any good. writing it sucked shit, it was effectively unlearnable.

i mewed a time or two about something like term rewrites or constraint handling rules as the type system. goofy, but old and studied, and the strongest part of ATS proofs in general is they stop you from passing shit where it doesn't go. (ATS in particular can attach proofs to FFI boundaries; you can actually state that C code is misbehaved or assert its well behaved and bring the proofs back in.)

eh i'll read the rest of the paper
Replying to @icedquinn@blob.cat
Replying to @icedquinn@blob.cat
Replying to @icedquinn@blob.cat
Replying to @icedquinn@blob.cat
Replying to @sun@shitposter.world