This is a great thread about how bitcoin miners in Texas help stabilize the grid during peak usage (summer and winter). The comments by Peter Todd are illuminating. The Economist article is a hit piece based on old and selective data. The comments explain why the Economist is wrong (again).
2 Likes
Has there been any significant progress toward using Bitcoinâs purported Turing complete semantics to implement smart contracts general enough to support something like Silk Road? I ask in part because while wondering what became of Nick Szabo (who went all-but-silent on social media a few years ago) I ran across the above article that, in the process of debunking the idea Nick is Satoshi (which Nick has also denied), linked to a video demonstrating Turing capability which Nick seemed to deny in a prior public appearance.
While I didnât follow that demonstration (no time to think about it in adequate depth) there does seem to be pretty wide-spread confusion about Turing completeness due, mainly, to the fact that all computers are finite state machines which means they are not âTuring completeâ. This gets into the hardware software distinction where software supports âcodesâ that may or may not have Turing complete semantics, regardless of whether this is a hardware fiction. Said fiction is central to any âout of memoryâ condition in any program, and the associated exception handling.
This, further, is central to the profoundly destructive claim that because the Algorithmic Information Criterion is âarbitraryâ because of the âarbitrary choice of UTMâ â a claim that is intuitive nonsense on the face of it if one simply considers the fact that the natural sciences use arithmetic â the axioms for which are not âarbitraryâ in any but the most vacuously pedantic sense. This is what drove me to concoct NiNOR Complexity
NiNOR Complexity is of some theoretic interest in its own right but it should not have been necessary to concoct it to nuke the social pseudosciences and get on with solving the TFR catastrophe:
2 Likes
1 Like
2 Likes
Yeah you canât automatically prove smart contracts correct if they use Turing complete semantics for the same reason that you canât generally prove programs correct: The halting problem always gets you. But the same is practically true for finite state automata for the obvious reason that any computer is a finite state machine because itâs finite. This problem always arises in business process formalization. Itâs complicated. This is one of the reasons why when Firemanâs Fund wanted to go paperless I suggested empirical capture of the business process, shipping digitized documents around on floppies keeping the physical process in place as much as possible, rather than relying on business process experts. And then gradually automating from the bottom up keeping fall back positions all the way back down to paper. I was not popular.
Relying on an abort mechanism like gas or in the more general distributed programming case timeouts (including state transition counters with limits) requires some kind of atomic action with rollback mechanism. Then you get into the whole distributed database ACID problem for which the blockchain is not suited. This is similar to the problems that arise in business process specifications where exceptional conditions occur.
A few years ago I actually put together a business plan for a company that would engineer smart contracts going back to first principles of logic programming with a four layer stack formalization: business process at the top talking to lawyers and a blockchain at the bottom with logic programmers â traceability throughout. Some of this I had done back in the '80s when representing the transportation sector to the Science Applications International software process committee pushing first order predicate calculus as specification language.
Frst order predicate calculus canât express Turing complete semantics without a wonky global State variable being passed around through all the predicates doing infinite recursion.
There are some coins out there resorting to proof assistants like Coq but Iâm not really competent to comment on them for the same reason Iâve never really understood why everyone loves type systems so much. It seems to me the types are just syntactic sugar for another kind of predicate.
2 Likes
https://cointelegraph.com/explained/what-are-bitcoin-covenants-and-how-do-they-work
Covenants are a source of contention in the bitcoin developer community.
I donât have an opinion on covenants because I am too lazy to study.
Peter Todd is a credible person on almost everything related to bitcoin improvement proposals.
https://x.com/peterktodd
1 Like
This is an idea thatâs been kicking around since the 1980s when people first started talking about e-money systems. I think Coevolution Quarterly carried an article on one idea like that back then. The problem is in direct conflict with the marketâs liquidity-based price discovery.
You might be able to ameliorate it somewhat with an idea Dan Brumleve and I were kicking around circa 1998, a prototype for which won an award at the 2000 Hackerâs Conference called dbarter (distributed barter). Basically you just give up on uniform currency and try to make barter work with a ridiculously complicated exchange rate system with no market depth, so everyone can offer stuff from their own âbankâ (ie: inventory of goods and services). I was interested enough in the potential of that approach that I basically turned down a chance to sneak into the Paypal Mafia because I thought their little âpaypalâ device to be inferior. Well, it was inferior to what they eventually ended up doing with the banks and the website. And the dbarter prototype never really caught on. Dan ended up rewriting Napster for Shawn Fanning with me encouraging him to try to minimize the size the binary as a demonstration for what my intuition was telling me should be the metric for software quality assurance. I still have dbarter and Danâs Napster version if people are interested for historic reasons.
But that was 25 years ago and my thinking has progressed to the point that I now consider property money (fiat bound to property rights) to be necessary for civil society. That gives a new spin on âgoldâ as âbarbarian moneyâ â and I suppose that holds for BTC as well.
3 Likes
https://www.axios.com/2024/12/25/russia-bitcoin-evade-sanctions-crypto
Russian companies are using bitcoin to evade Western sanctions, thanks to a new law, the countryâs Finance Minister Anton Siluanov confirmed in a television interview.
3 Likes
Axios is mostly fake news. The chance of this story being true is roughly 50/50. The text at the Siluanov interview page has nothing to do with BTC; itâs about infrastructure spending and the budget. Since I donât speak Russian, I canât know if the interview has any mentions of BTC.
3 Likes
Good point about Axios⌠here is another source, Watcher Guru:
3 Likes
1 Like