True. It is worth pointing out that Isabelle/HOL does not have dependent types in its underlying logic making framework building a (much?) harder work.
Despite being based on semi-functional programming language Scala, I found no evidence that the language AxLang has anything to do with formal verification. I may be wrong, but what I see now is lots of promises without any details.
GitHub feels so much like some social network site. It has too many distraction factors for any thinking person, that's why I hate it. Bitbucket is a real thing. Go get it, stop being a GitHub hipster today!
Authentication of a write operation is not the only problem a blockchain system solves. Using a public blockchain, for example, you are assured that:
0) all writes are authenticated
1) all the data written will be accessible to anyone
Now contrast it with a centralized solution where admit can just restrict access to some data. Yes, all writes are authenticated, but who cares if you cant access them?
2) The history of all writes is also reliably preserved and accessible to anyone.
3) In case of smart contracts, the business logic is visible to you upfront. You can study the contract and decide if it is fair to participate. You can study the history of that contract also.
4) All "redundant" nodes have proper incentive to participate in the activity. They gain value just by validating and processing your transactions.
My point is that this is just not achievable using traditional DBMS: the original premises ("trust model" and incentive model) of those systems are very different.
Interesting point, thanks for sharing. But, anyway:
What incentives do those mirroring nodes have to store regular data blobs and process requests from clients?
Who will decide the privilege to be such a 'mirroring node'. The origin can run several such 'mirroring nodes' and rewrite history on all (some of) them: how would you know who is giving you the truth in case of conflicting information?
I bet if you solve those questions, you will be simulating a blockchain system. Do you agree?
>But of course, if this is the case, then it begs the
>question of why a blockchain is even needed. Just use a
>shared database.
Two issues regarding your second observation.
1) A change that requires a consensus among some non-tiny group of participants is not trivial thing to accomplish in practice. You will have to wait before every one from a group of N (say, 20) representatives will agree with your change.
2) Why a blockchain is needed? Because no other "shared database" provides the same trust model which is "everyone trusts no one". Every other database "security model" in existence assumes that every admin trusts every other admin. If it is not so, then things quickly become complicated and impractical.
I wonder how one may prove that a thing originates from some specific place? I mean, you have to have some kind of trusted by all parties external observer who will assure that fact. Am I wrong here?
If a supplier is running its own blockchain, then it really makes little sense. But to gain real trust of its clients, supplier will actually put it on a public blockchain. Only then external experts will say: "yeah, this supplier is really trustworthy". In other words, the incentive to use a public blockchain instead of their own, private one, is to gain real trust.
By using such BC solution, you can be sure that you eat a fish caught by some certified supplier and not by some poachers. A certifying body is assumed to check ethical questions.
When you have a need to establish some business procedure between different parties that do not trust each other, smart contracts might be very useful. No other database is able to provide guarantees/features comparable to the public blockchain in that respect. A trust model of most modern databases just do not comply with "everyone trusts noone" principle.
About relying on Intel SGX. Yes, blockchain oracle to be trusted needs to be run in some kind of protected environment. So what? It doesn't imply that technology is useless. I would say, we have a synergy of different security technologies to get really impressive results.
It is a bit out of topic, but anyway: Is it possible to defend a PhD thesis without taking a graduate program at all? Imagine an industry researcher without a PhD degree who is willing to obtain one.
Oh, sorry for that, the question was misunderstood.
I presume that a user-level contract language like Simplicity is going to be translated into low-level byte code like EVM. That low-level code is what gets executed on the blockchain. People can choose other languages with less guarantees, write contracts in those languages, and those contracts will be interoperable with each other. This is how things work right now. In my view the real problem is to introduce a language that will be both safe and expressive at the same time.
I can program a contract that can be parameterized with an address of some other sub-contract (then, say, store it in variable), which I call to do some particular logic. If I change that sub-contract address, I can effectively change my contracts logic. Is that what you?
I would like to mention an interesting paper regarding the topic:
Marino, Juels - Setting Standards for Altering and Undoing Smart Contracts (2016).
I see your point about 'pure notions of correctness'. While I agree that some interesting properties of a contract is not easy to come up with (and hence verify), I still believe that there are some 'safety' properties which are far easier to articulate.
I also believe that there is an element of modeling: it may be a viable way of validating properties.
I wonder if your advice can be applied in non-google setting? For example, in some general enterprise company.