Home | Notifications | New Note | Local | Federated | Search | Logout
Note Detail
Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-10-10 07:16:17)
@icedquinn have you seen this https://bend-lang.org/
it's kind of funny that the adoption of proofs is going to be to help vibe coders, which I mean, not even ironically, this is all achieving what computer scientists wanted, for the lowest-common-denominator, but with the result of reliable software to solve problems, not jerk off about typing in a console
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 07:18:57)
@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.
Reply
---Replies---
Blurry Moon@sun@shitposter.world (2026-10-10 07:20:18)
@icedquinn bend is interesting but I might be vibe coding something similar for my specific needs
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 07:21:30)
@sun i think i've poke claude (but not GLM as much) about it. Lean upstream uses LLMs for proofs, but its safe to do this. they write the term to be proven by hand and let the LLM close it. so the LLM never controls the end goal and the kernel validates intermediate steps are valid.
it is less safe if the LLM is writing the goal because you can--even with dependent types--make a spec that is ass trash and worthless.