Readit NewsThough, there is also the Ackermann function... so for some recursive functions it is not be as easily seen why they would terminate.
> Related, Typescript is the only language I know of that through flow analysis does not require you to redefine the variable. E.g. you can do something like
This is called smart casting and is widely used in Kotlin
Starting from simply typed lambda calculus ("simple type theory", also "higher order logic"), one can make various extensions that make the logic language more expressive. The lambda cube is a way to systematically organize the space of type theories.
Interestingly, the theory has become very relevant for type systems of normal programming languages. Milner invented ML as "meta language" for helping with logic and theorem proving, but it was used widely and today everyone expects generics to work more or less as in System F polymorphic lambda calculus.
Satoshi wrote about this architecture early on in scaling the blockchain. Ethereum also allows light clients and I think it even has checkpoints that make downloading headers faster. Cryptographic protocols that verify smart contract results could be included in Metamask. I feel like not mentioning this in the essay shows a lack of familiarity with the literature even if he was extremely opened minded (enough to create dapps himself.)
He did make valid observations about third-party trust: OpenSeas and Infura. But in both cases: these protocols can be implemented without centralized architecture. A decentralized alternative to Infura (that provides reliable results to users and easy-to-check attestations) is possible to build. One should also note that in blockchain land the lack of incentives to run a full node is a problem people are working to address. It's actually a perfect illustration of how the blockchain can lead to emergent systems. Some ledgers already have rewards for running full nodes. So yes -- people do want to run full nodes -- they just want to be paid for it.
The problem is that benefits of well-thought out incentive systems evaporate when access is mediated. If every dapp comes with its own mobile client and app-specific servers to address this, there is nothing decentralized about it.
In general, it could be appealing to have an open, established process for gathering public feedback on articles. It seems a scientific community would rather have their own version set up, where they could also curate content (rather than browse by category).
It's true that the so-called "folk knowledge", knowledge that exists in the community but no one bothers to publish in the form of papers, is a real problem, but at least in my field, it's by no means the majority of knowledge.
As someone from a peripheral university where you can't just drive a few miles and talk to the best in your field, I have successfully started in new subfields of study (getting to the level of writing research papers in top-tier venues) by reading the literature.
While this essay provides a very interesting point of view, I suspect it's heavily colored by the authors' failure to monetize the technology (which is related to the fact that people doing most of the grunt research work, who would benefit the most for this, are PhD students and postdocs who have no money to pay for it - in the text, the author hints at this). I wouldn't take it as an accurate description of academia.
The equivalent to those biomedical industry players are the big tech who develop closed source and push the edge in some area. They will publish but that does not mean you can replicate any of it.
Software is also fragmented, crippled by IP lawsuits, patent trolls and so on. This does inhibit ability of society to benefit from software since it depends on the private sector to sort things out. The PhDs go and build businesses to "make the science work" in that sense.
The ideal of detached pursuit of knowledge is not a complete fiction (despite the hyperbole), but it does remain an ideal that can only be approximated.
This is the world we live in. A scientist is a person that needs to make a living and is subject to various constraints.
The reason that there is little money to be made is that society hasn't found a way to set up the scientific process in such a way that the constraints would value the increase in public domain knowledge higher than the incentives to hold some knowledge back.
Part of this may stem from leaving specialized knowledge to academia while letting only companies reap the monetary rewards of putting the knowledge to use. Society benefits only indirectly (better drugs, machines, etc) but industry players will rather shield knowledge and adapt its representation to their own needs.
Doesn't this work: consider the call graph of all possible argument lists (with an edge A->B if f(A) calls f(B)). If the function terminates, there are no cycles, so this is a DAG, which puts a partial order on the set of argument lists which strictly decreases with each call.
Yeah, if you know that the recursive function always terminates, then you know that each recursive call makes the set of remaining steps strictly smaller.
When you want to prove termination, then it is exactly what you need to show (that the remaining work does get smaller, no cycles).