Viewing profile — 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 b…

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 wha…

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 be…

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 authenticate…

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…

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 …

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 fac…

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 th…

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…

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 wil…

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 …

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 chan…

> 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 pr…

>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 t…

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 p…

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! :)