Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
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
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:02:51)
@sun :blobcatpensive2: hoare and separation logic. that's not what makes something formally verifiable, but it helps.
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:02:38)
@icedquinn my main constraints for this language were: typed capabilities; amenable to future simple formal verification; simple implementation
Reply to @sun@shitposter.world
ooignignoktoo@ooignignoktoo@shitposter.world (2026-08-22 10:02:22)
@sun such a good skit
---Attachments---
image: https://media.shitposter.world/shitposter.club/46/d7/66/46d7669854d55857559ee11f676896128b21d3ec2fee8ad62d921a74df319e5c.webp?name=kao_QPz61s6LBQ.webp
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:01:21)
@sun i don't think you need any of the above to qualify as formally verifiable, either. it just means a static analyzer can make guarantees. some of the restrictions in aviation code are because those particular things are both good at hard real-time and also obvious to reason about (type pools in ada mirror how hard real timers actually reason about code) and static dispatch tables have every jump target known at build time
Reply to @ooignignoktoo@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 10:01:18)
@ooignignoktoo he STOLE it
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:01:08)
@icedquinn really simple, set of annotations to state valid inputs and outputs, expected outcome of loop operations
Reply to @sun@shitposter.world
ooignignoktoo@ooignignoktoo@shitposter.world (2026-08-22 10:01:01)
@sun Where exactly did he get the bike?
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 10:00:09)
@icedquinn I might eventually vibe code Austral compilation for FRUTE
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:59:41)
@sun pony claims to have capability types. i guess that's what it has, though i don't see them called that elsewhere. viper has fractional types (values have shareholders, only the 100% shareholder can mutate, but you can allot out shares and each slot is now read-only until merged.) Isabelle does higher order logic (HOL) which is basically predicate logic kernel where you have a tiny set of privileged operations that produce axioms and facts and then further facts have to be derived. Agda/Idris/Lean/Coq have dependent types under some curry-howard thing. ATS does the curry-howard thing, but then proofs are themselves ghost code which have linear types (must be used exactly once.)
austral does linear types and its how i initially learned about them.
ATS i think gets this the most intellectually correct, because proofs are threaded through the code. you don't prove some functional copy of the program does things, you state proof requirements at the call sites and provide proofs like they were data. which makes it tenable to carry proofs in imperative code, as ATS is basically "C with dependent types and god's shittiest ML dialect syntax"
dumpster rapist@themilkman@shitposter.world (2026-08-22 09:59:35)
while killing your child is absolutely horrible and inexcusable, there is a definite problem with post-partum depression, yes.
i think new mothers who will often not have their husbands there, and extremely often completely lack any support network (their mothers, sisters, aunts and cousins and other relatives) and have to deal with raising a baby completely alone will probably be unhealthy mentally and physically.
do not fall for the internet drama nonsense of "it's just foids wildin!!!!!" or "it's okay to kill babies!!!!", try to look for rational causes and then solutions.
our modern world is completely horrible right now, and it hurts me to say this, while modern women don't want to take accountability, neither do modern men.
if you claim i am a feminist libtard you prove my point, stop engaging in internet niggerbabble, it would be better if you shut your mouth.
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:54:42)
@sun idk what that means. pony types?
formal verification has many names underneath.
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 09:52:41)
@icedquinn I needed a pascal-like capability language that had a narrow formal verifiable subset
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:51:33)
@sun i did something like that out of Io, but its been a week or two trying to get executive dysfunction to let me finish the parser :blobcatghostrev:
going back to being jobless and then being shoved in to windowless rooms was really bad
Reply to @ElDeadKennedy@shitposter.world
Blurry Moon@sun@shitposter.world (2026-08-22 09:50:15)
@ElDeadKennedy the last time I worked on a house, the dumb fuck before us glued down foam backed carpet to hardwood floors
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 09:49:31)
@icedquinn I specced out a dumb little language to make it easier to bootstrap a self-hosting compiler on my FRUTE arch
ElDeadKennedy@ElDeadKennedy@shitposter.world (2026-08-22 09:48:45)
I have to remove 40-year-old wallpaper
---Attachments---
image: https://media.shitposter.world/shitposter.club/4a/f6/1c/4af61c69aa40723980edf449062404ebe5b44ac49479c422308140bef4ccb19f.webp?name=GNpI39WpcVUvvw.webp
Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:48:23)
@sun meanwhile my dumb ass slowly learning formal methods instead :comfystoner: "the kernel should be written in ATS"
Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:43:50)
@sun https://blob.cat/notice/B9Zumh2QZl0bgxnR1k its a pretty stupid thread
basically goes "AI bad, LKML bad" to "we should use civilized tactics to dissuade devs" to suddenly whiteness. extremely retarded shit. lefties cannot win shit until they give up this idea that victory is entitled.
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 09:41:32)
@icedquinn wat
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:34:11)
> people are calling us facists we're just defending the commons
if everyone is calling you a fascist you should probably take a half moment to contemplate why that could be :blobcatgoogly:
Alviro Iskandar Setiawan@viro_ssfs@misskey.id (2026-08-22 09:34:00)
Doh, she confessed it! I wonder how Bell's relationship with Aiz Wallenstein will go after this. Who will be the chosen one in this romantic story? As season 5 already tells us, Syr is out of the running. So I think the options left are Hestia, Aiz, and Ryuu.
I am looking forward to seeing who'll be Bell's wife!
Title: Dungeon ni Deai wo Motomeru no wa Machigatteiru Darou ka Season 5, Episode 13.
---Attachments---
video: https://obj.misskey.id/media/c3fb5a26-368a-4505-9336-b3b99957a76b.mp4
Blurry Moon@sun@shitposter.world (2026-08-22 09:22:03)
---Attachments---
image: https://media.shitposter.world/shitposter.club/f0/b4/da/f0b4dad45fe6917a405c12d0d392256cd1346dc216bd9c5e58c1ee35c88cdf69.webp?name=LnS5GzpNoT3sWg.webp
Blurry Moon@sun@shitposter.world (2026-08-22 09:19:41)
in every man's life there is a time when he must say "I need to write my own programming language to address this"
Older Notes