unboxed_type

What is a "promotion committee"? By saying promotion, are you talking about transitioning from "engineer level 1" to "engineer level 2" kind of thing?

I wonder if your advice can be applied in non-google setting? For example, in some general enterprise company.

Are you talking about CertiCoq project? It is not ready yet and not clear when will be.

[1] https://www.cs.princeton.edu/~appel/certicoq/

Listen to this wise man, he knows what is speaking about.

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!

Whats the business model behind that kind of activity?

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.

Please correct me if I am wrong somewhere.

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?

Thanks for that quote!

>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.

Why not to use already running platforms like Ethereum where all those incentive issues are already solved?

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.

Most probably because of a lack of functional programming mindset.

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.

> it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.

I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.

>In fact I don't even understand why a blockchain language must emphasize provability.

For two reasons:

1) A smart contract can not be changed in a BC after deployment, so it has to be correct up-front (I am not sure if this fact is obvious for readers, so I decided to add it).

2) A compiler is able to deduce only a limited set of properties. Actually, the less expressive language you have, the more properties you can deduce at compile-time.

The proposed language have chosen to be less expressive to get a higher degree of decidability. But, in my opinion, it goes to the extreme where it becomes no longer useful. The real thing would be to find the right intersection of decidability and expressiveness.

It is far from solid and yet it is easy to understand (modulo corner cases) . I doubt that lambda-calculus-like language will take over it just because it gives one an ability to prove correctness properties in Coq.

I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)

It is hard to imagine that a proof-assistant will be used as a tool for checking smart-contract correctness due to a lack of sufficiently trained personal. What this BC community is really need is a suitable programming language which will be tailored for functional correctness and expressiveness. Unfortunately, the Simplicity language addresses only the first half, and it is not sufficient for practical success IMO.

I do appreciate the author's attempt to create a new worthy language really, I do a research on this topic myself.

What concerns me is that the presented language is not suitable for any practical programming. Even for the most simple smart contracts, the final Simplicity program will be huge and unreadable due to the lack of familiar data structures and constructs. The language resembles me some kind of lambda calculus which is good for theoretical investigation, but not suitable for practical stuff. I am not ready to exchange a language convenience for better provability: it must have both issues addressed at the same time, only then the mix will be right for an end-user.

And what do they call mathematics. Is it about machine learning/big data specialists?

Sounds interesting. Reminds me "Artifacts Evaluated" stamp.

Very interesting idea, clearly explained use-cases, thanks!