Conversation
Q.U.I.N.N.
icedquinn@blob.cat
somebody asking why do formal methods instead of extracting things from source. the researcher just verbally stared at the person. 
odd thing about TLA+ type shit is you're not really meant to code the whole thing in that. you are absolutely meant to paper over implementation details symbolically. its a way of saying, like, "given how we're thinking of making the chat room sync is there any situation that will cause a complete meltdown" and it just kinda sits and grinds out all the permutations of what you've identified as failure points to see how they could happen.
fizbee even has a cool thing where it will write unit tests for you based on this.
odd thing about TLA+ type shit is you're not really meant to code the whole thing in that. you are absolutely meant to paper over implementation details symbolically. its a way of saying, like, "given how we're thinking of making the chat room sync is there any situation that will cause a complete meltdown" and it just kinda sits and grinds out all the permutations of what you've identified as failure points to see how they could happen.
fizbee even has a cool thing where it will write unit tests for you based on this.
1
0
0
Q.U.I.N.N.
icedquinn@blob.cat
@nuukaset i understand the theory. TLA+ is a bit obtuse.
fizbee pretty much just ports TLA+ away from lamport's crazy notation and java stack.
fizbee pretty much just ports TLA+ away from lamport's crazy notation and java stack.
1
0
0
Tiskaan
nuukaset
@icedquinn nah i just remember reading a textbook about people making model checking systems and i thought about how they would compute a shit ton of permutations to verify software and it scared me
1
0
0
Q.U.I.N.N.
icedquinn@blob.cat
@nuukaset lamport wanted them to use a theorem prover but afaik TLAPS never really materialized as a whole product. its there, incomplete, and they just run the brute force part.
i think i looked at a similar design that sadly did a lot of the same. use lua calls to generate new graph nodes, and the runtime harness tries its best to schedule which frontiers to check in some configurable way.
then again TLA+ wants to prove a model is safe whereas graphstrolabe was more meant for discovering strategies
i think i looked at a similar design that sadly did a lot of the same. use lua calls to generate new graph nodes, and the runtime harness tries its best to schedule which frontiers to check in some configurable way.
then again TLA+ wants to prove a model is safe whereas graphstrolabe was more meant for discovering strategies
1
0
0
Q.U.I.N.N.
icedquinn@blob.cat
@nuukaset the idea was basically i can tell you in a given world state what the next likely outcomes are, and i can tell you how desirable a given world state is, but i cannot tell you what timelines will actually happen.
so the design is meant on generating timelines to some horizon limit and compacting them back with analytical statistics. "of the ?? timelines hallucinated, we won in 7 of them" kind of shit. afaik that isn't a project that exists, but its also for a very specific kind of person
so the design is meant on generating timelines to some horizon limit and compacting them back with analytical statistics. "of the ?? timelines hallucinated, we won in 7 of them" kind of shit. afaik that isn't a project that exists, but its also for a very specific kind of person
0
0
0