Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:46:54)
@icedquinn sometimes I fall into the "actually you're complaining about being forced to eat goose shit not chicken shit, your argument is invalid" argument form
:conga_parrot::conga_parrot::conga_parrot::conga_parrot:@mrsaturday@shitposter.world (2026-08-22 10:46:15)
Your timeline has been visited by the Pizza Squirrel
Big slices and fresh toppings will be yours if you post
"BON APPETIT PIZZA SQUIRREL"
---Attachments---
image: https://media.shitposter.world/shitposter.club/6d/f9/7c/6df97c911e4ac89f816d398ba9dc662276605e916db37901a9e46f1faaa11384.webp?name=ibNb1-HOsYxWwg.webp
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:46:02)
@sun to be fair most of finance is degenerate gambling with sophistic blither
Reply to @sun@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:45:55)
@icedquinn strawman is obsolete because we have the internet now and if someone says "nobody believes that crazy version of my belief" you just direct them to the subreddit of people saying it
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:45:08)
@icedquinn arguments: everything is strawman
finance scams: everything is ponzi
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:44:20)
intellectuals dying to jump on the only fallacy name they remember (strawmen) to explain someone's actual lived experience
Reply to @subnetter@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:43:36)
@subnetter @nimrod disclosing serial killers and spree killers causes copycat killers every time so they stopped
Reply to @nimrod@shitposter.world
renellen@subnetter@shitposter.world (2026-08-22 10:40:44)
@nimrod
What are you talking about ? Several studies and research have led to the conclusion that there are more than we currently know about at any given time in America alone.
And if you lived where I did growing up, you would also be aware of serial killers that aren't disclosed to the public.
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:39:50)
@icedquinn I appreciated it
xndrive@xndrive@misskey.id (2026-08-22 10:33:24)
ngewip 😭
---Attachments---
image: https://obj.misskey.id/media/8eb15083-5d1d-4687-97f9-f3002d7d99e3.webp
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:30:48)
@sun i will now stop talking about this :gutkato_zipita:
Reply to @subnetter@shitposter.world
nimrod@nimrod@shitposter.world (2026-08-22 10:30:08)
@subnetter Weird how there were only like 5 major serial killers and then the media just decided it wasnt newsworthy anymore.
Yukari :role_nsfw: :verified:@y@misskey.id boosted:
@5modj@misskey.io (2026-08-20 00:14:00)
misskey来た時に描いた村上どん(再掲)
今度:chief_impact_officer:丸出しのNSFW描いて村上さんを辱めるか
---Attachments---
image: https://media.misskeyusercontent.com/io/439c3520-e284-4d95-8141-261731c23cdb.webp?sensitive=true
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:27:15)
@sun idk the short answer is read as much of why3 and agda/idris/lean/coq as you can stomach and go from there. lean might be the easiest because they actually want to ship product, so there's docs aimed at programmers. those are proofs through functions. souffle is used for a lot of analytics in some spheres, which is basically a huge datalog engine where you "compile" the program to a fact base and then write queries about it.
the most accessible weapons are why3 and souffle, in that you're dumping the program out to a different imperative language (whyml) or dumping the somewhat compiled IR in to facts (souffle) and then writing claims about it.
the lightweight weapons are reasoning about what the heavier weapons can prove and finding a way to make the failure states inexpressible without them. pony doesn't need theorem provers because he already proved the type system cannot express the failure states pony is intended to prevent, so it can get by much more cheaply by just committing to that type system.
this is ultimately why some languages get mad about stuff like pointer arithmetic. if you can do arbitrary pointering, you can no longer make static guarantees about points-to. (points-to analysis is a big deal in verification, there's specific optimizations in datalog literature to cope with the sheer number of pointers and their potential pointer locations.) some of the aircraft (where verification thrives) rules don't allow closure magic at all because its difficult/implausible to present a fully static CFG for them. (continuation passing has no implicit guarantee that code will ever resume in any meaningful way, although its possible to make them do so)
(the lightweight version also tends to shape the language and is inflexible, sadly, so unlike ATS you can't come back in the future and alter the axioms for a specific project.)
ivy@ivy@misskey.id (2026-08-22 10:26:51)
ivy search
ivy@ivy@misskey.id (2026-08-22 10:24:58)
dreamt about disasters
ivy@ivy@misskey.id (2026-08-22 10:24:43)
beras pemerintah
Yukari :role_nsfw: :verified:@y@misskey.id boosted:
@fastest_yukkuri@misskey.io (2026-08-22 00:23:43)
「バニーキツネメイド参上！」
「要素多くない？」
---Attachments---
image: https://media.misskeyusercontent.com/io/8d1b7001-a63c-4530-a7b7-a1cb8fef0064.png
Yukari :role_nsfw: :verified:@y@misskey.id boosted:
@minoson@misskey.io (2026-08-22 01:19:09)
ガシャポンで売ってたヘッドドレス
---Attachments---
image: https://media.misskeyusercontent.com/io/webpublic-423db79d-80c0-4497-b2ea-699b5af15d6a.webp
Reply to @nimrod@shitposter.world
renellen@subnetter@shitposter.world (2026-08-22 10:22:04)
@nimrod mommy issues in men creates serial killers
Reply to @sun@shitposter.world
nimrod@nimrod@shitposter.world (2026-08-22 10:19:16)
@sun @subnetter @themilkman >woman has depression
>kills someone else
---Attachments---
image: https://media.shitposter.world/shitposter.club/c3/a2/3a/c3a23a831f1ac707ed99e87a70372e7cb7f1c89c6e448af9ec1115d171e36960.gif?name=zuzcpdYOdxqwzQ.gif
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:15:38)
@sun i don't think this is a downside because logic systems always live with the ability to "prove false" with bad axioms, so "bring your favorite logic layer" isn't adding any more danger than already existed. it's just making dependent types a dime store implementation instead of intellectual masturbation
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:14:48)
@sun i have some notes on "scriptable types" which was basically me just asking can we have discount dependent types as machinery without the appeal to hypothetical perfection.
nelua shows that letting you write to the AST is neat (not just "create code via macro" but they were lua tables, so macros could stash metadata in there for other macros.) ATS has two "universes" for ghost code and compiled code. (why3 and dafny call it "ghost code," because its a ghost, it exists to prove things to the compiler but it doesn't make it to execution.) so we could simplify it to 'ghost {...} runs ghost code' and 'ghost types are ghost code', and type checks just become 'run some code in the compiler's VM'.
nelua already does this with concepts; a concept is AST fed to a function which returns true or false. useful for metaprogramming, but instead of generating code we're vetting it.
its an interesting line of notes because it means you can get the core value of dependent types for much cheaper than people usually pay, though you have to bring the rigor separately
Reply to @subnetter@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:13:53)
@subnetter @themilkman I have avoided spouting off on it because
1. I don't know all the details and the details matter
2. post partum depression is real and its not just women being crazy all the time or something
3. obviously not justifying murder but it's a sensitive topic for real people who experience it, doesn't need to be my recreational discussion topic
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:10:05)
@sun it largely means that you can make proofs about particular concerns. there are many ways to get there.
hoare logic is all about pre/post conditions, separation logic is basically that with some extra operators about splitting up a heap. they are ways to relate programs to formal logic.
HOL is sort of the easier formal logic since the kernel is just "true because we said so" and a couple of "true if these other facts were true." isabelle/hol has the sledgehammer which auto-derives a lot of proofs by SAT solving.
dependent types are basically turing complete macros, so they are cursed. i don't quite know how lean and coq deal with them; i think there's a proof layer and the code layer and they mix in some sideways means. ATS the proof is a value, it just doesn't exist at runtime, so some parameters exist at runtime and some don't, but it makes it neat and explicit.
what pre/post conditions do is basically let you outsource some proofs to why3. you write a compiler backend that spits out WhyML code and let Why3 outsource the checks to Z3 et all. this works great for some stuff (linear ranges and set memberships.) it can fall back to coq proofs for gnarly shit.
there's also souffle, but eh
Reply to @ooignignoktoo@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:09:18)
@ooignignoktoo people memed the shit out of this when they made a black Dr. Who
how did he get the Tardis???
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:08:30)
@icedquinn yeah really trying to make sure its amenable to static analysis
Reply to @themilkman@shitposter.world
renellen@subnetter@shitposter.world (2026-08-22 10:04:31)
@themilkman I agree with everything here except for the comments about women trying to avoid accountability, I have yet to see anyone comment as such as fediverse. People are shouting into an echo chamber based off social media comments while the case is actively unfolding.
But thank you for actually having the courage to call this shit out for what it is. Pretty depressing to see people make a spectacle of this tragedy for their own political reasons or biases.
Also insane that most people speaking on the topic are also willfully ignorant to the fact that they likely know a woman who struggled with this, if not their own mother's.
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:03:12)
@icedquinn yeah
Reply to @sun@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:03:06)
@icedquinn no actual formal verification is happening at this stage, just added annotations to make it easier in the future. I don't know what I'm doing tbh
Older Notes