They extract from Coq to C. Like in my Brute-Force Assurance concept, that would let us confirm and supplement the formal verification by hitting the C output with every V&V tool for C programs that we have on hand.
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.
How do you mean? There are examples of formal verification working in the video. The resulting compiled smart contracts are on the live Ethereum blockchain.
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!
I used bitbucket at my last job and it felt like an under-performing Github the whole time. Code reviews were much more painful, the UI was not as intuitive, it's slower and if it has a "search this repo" function I couldn't find in the 2 years I looked.
People don't use it because they are hipsters they use because it works well.
I use gitlab (and to a lesser extent github) at work now and IMO gitlab vs github they are about equal in terms of ease of use and "just working like you expect."
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?
I wonder if your advice can be applied in non-google setting? For example, in some general enterprise company.