pull down to refresh
adam back: muppet
john carreyrou: useful idiot
it's the usual pattern where the suits ride the coattails of the devs and leave them holding the bag.
blockstream may have the dubious honor of joining that club.
If you peel all the layers back it's just affinity and riding coat tails, this fraud (if it is indeed one) and pretty much every other.
Back has a halo and is somewhat of a dupe, so he will be milked by bad guys until the cow dies.
that's the usual pattern anyway.
too early to say if it plays that way for blockstream. but many red flags
"In the light of persistent disagreements among the maintainers and a contributor,
all the parties agree to submit their disagreement to a neutral meditation to seek
a common solution, at a physical place of hearing being convenient for all the involved
parties."
Nice.
Feels like resistance to
https://en.wikipedia.org/wiki/The_Tyranny_of_Structurelessness
which imho has to some degree infected core. And I say this as somewhat that likes and uses core.
But it is great to see other competing bitcoin clients coming online.
Hi @Scoresby or @Murch or or @justin_shocknet or anyone else interested in this stuff.
I am working on a tlaplus formal verification of bitcoin. I will probably push it to delving bitcoin or the ML soon, but it's not quite ready to hit publish yet.
I'd love to get a second set of eyes or peer review though before pushing it out, so if you would like a peek dm me at thomashartman1 ( at ) gmail.
In terms of the usefulness, tldr and imho: very useful.
https://www.youtube.com/watch?v=Fq5EQBFLEC8
"If you're not writing a program, don't use a programming language"
Leslie Lamport, 6th Heidelberg forum.
another good one is his "thinking above the code"
IMHO for bitcoin it's not so much proving things correct, as giving precise meaning to what code SHOULD do, rather than comments in english and then code that hopefully fulfills what the comment says, if the comment or code haven't drifted out of sync.
IE, tlaplus is a much better pseudocode.
Communication and clarity is the primary benefit.
Proving is style point / gravy.
Also in our brand new AI world, formal and precise spec gives much better mechanisms than english handwavy prompt + some tests (probably gamed by AI) to keep the codegen from running off the rails.
Also, it is now much easier to write the specs themselves, with AI "specgen."
tfttv?
you mean tftc?