Meetup "Smart Contract Formal Verification", Europe/Ukraine/Kharkiv, 4 July

golovach-ivan commented 6 years ago

Holding tech/math meetup in Europe/Ukraine/Kharkiv, July 4. Topic: "Smart Contract formal verification: Process Calculus and Modal Logics".

Event Program

Tell about the RChain Coop.
Tell about bounty program.
Tell about "Designing Computational Calculi" course.
Big topic: Chemical Abstract Machine, LTS and CSS.
Big topic: Propositional Logic, Predicate Logic and Hennessy-Milner Logic.
Intro into Pi-calculi + Caires/Cardelli logic.
Intro into RHO-calculi + Namespace logic.

Benefit to RChain

Set up local dev/math commulity (Kharkiv, 1.5M population, engineering city, 15k-20k IT people).
Involving developers and mathematicians to RChain Coop (#775).
Develop a "meetup in a box" (#779) slides + practical tasks for Formal Verification meetups/techtalks.
Publishing video on youtube channel for 25.000 developers.

Budget and Objective

Involved

golovach.ivan - 75% kovmargo - 25%

Expenses

Publicity, Banners, Digital graphics $250 Hall renting $150 Camera and associated gadgets renting $80 Logistics $110

Estimated Budget of Task: $[1800] Estimated Timeline Required to Complete the Task: [3 days] How will we measure completion?

meetup video - published on youtube channel
slides - published into RChain google.docs

kovmargo commented 6 years ago

According to this task, could you please provide me with a good quality RChain logo? I'm working on printed matter and going to use logo to add more value RChain Coop.

lapin7 commented 6 years ago

See https://github.com/rchain/style_guide_and_files/tree/master/print

golovach-ivan commented 6 years ago

The meetup was held. Video will be uploaded to Youtube Channel soon (5-6 July). The discussion with math community was productive - mostly about

Formalisms (calculuses, algebras, logics) designing.
Hennessy-Milner logic with recursion.

And many questions was arised, main one: Ok, ModalLogics/HML is native logic for checking behavioral types like safety/alive properties (deadlocks, livelocks, etc). But what about "data-processing examples" (like "sort(int[]): int[]")? How to encode

int data type
array
ordering
etc.

My current point of view: we need a collection of syntax sugar libraries over HML/Caires-Cardelli-Logic/NamespaceLogic for encoding all this "real life" stuff: int, array, seq, funtion, tuple, either, etc.

I think we need a deep research in this direction.

Ojimadu commented 6 years ago

@golovach-ivan this I see this issue and #822 are same why would rather have them splitted? Any difference between this and #822?

golovach-ivan commented 6 years ago

@Ojimadu These are two tech/math meetups in two cities, but with the same theme. I thought it would be better to separate them (different issues).

allancto commented 6 years ago

I have spoken with @golovach-ivan and i recommend voting the budget as proposed in the issue statement. Both @golovach-ivan and @kovmargo are new members so rewards voting may be delayed but the overall budget may be voted now.

Thanks! -@allancto

Actually it does not seem possible to vote for this issue yet- @dckc is that a bug?

Ojimadu commented 6 years ago

@golovach-ivan Alright, I get it now. Do you have materials on this as well?

@allancto I think your inability to vote might be due to this issue being in pay period 201807

golovach-ivan commented 6 years ago

This is my oversight, that the task was created in July. These meetups are the result of our work in June, is there any possibility of transferring them to June budget?

Ojimadu commented 6 years ago

Well, the meet up actually held in July so it belongs to the July pay period and the metrics for completion has not been achieved.

dckc commented 6 years ago

@allancto writes:

it does not seem possible to vote for this issue yet- @dckc is that a bug?

See #682 disallow votes on issues created after the current pay period

We're now in the July pay period, so you should be able to vote for this.

kovmargo commented 6 years ago

You can find printed material here: https://drive.google.com/drive/folders/1llu0D7iqd4Oh6QmC1ZXTLsIawRSBh3no?usp=sharing:

Where it is better to store this data?

allancto commented 6 years ago

@kovmargo thanks for your question. Please post in the "RChain Community Worldwide" folder, you'll find a subfolder for our Russian language community. Let me know by DM in discord if you run into any problems.

Thanks! -@allancto

deannald commented 6 years ago

@allancto "This RChain Community Worldwide folder"is good for consolidating printed materials/write-ups, but is there a plan to make this folder not only available, but known to the RChain Community or is there a better suited place to be publishing these materials for greater access and visibility?

allancto commented 6 years ago

@deannald the folder is for materials referred created by our Worldwide Community, from where the will hopefully be referenced by our Worldwide Community Forum as well as any others who reference them. @ICA3DaR5 , i don't see a sub forum for our Russian Language community, let's get that going so that @golovach-ivan @kovmargo can begin posting there and also cross linking with habr.com.

kovmargo commented 6 years ago

@allancto seems I don't have permission for edit "RChain Community Worldwide" folder. Could you please provide me with? Thx

golovach-ivan commented 6 years ago

Video Smart Contract formal verification: Process Calculus and Modal Logics, on 4 July 2018 is ready and placed on Youtube channel in separate playlist Blockchain with second video (5 July meetup).

golovach-ivan commented 6 years ago

Slides (will be finalized in the future for next meetups. This is the first version):

golovach-ivan commented 6 years ago

The next step of research after this meet is the Correct-by-Construction project. Issue #835.

ghost commented 6 years ago

@allancto Will do!

kovmargo commented 6 years ago

HI, guys! Sorry that I'he write this here, but how can we get the reward? What we need to do next? What is the process of? It's not clear (

allancto commented 6 years ago

@kovmargo @golovach-ivan there is a vote on budget. You may vote and ask people who respect your work to vote now and up until the 8th of August. On or after the 9th you may submit an invoice for the voted amount. I'd recommend editing the issue statement above with a full description of the work you did and how you would like to be rewarded so that people may vote intelligently. For instance, if by your meetups you create people able to write smart contracts for rchain cloud apps (dapps) that's a high perceived value in our Cooperative right now. So are validator nodes and several other "hot topics". If you are able to form teams to accomplish this sort of work that's of high perceived value. Describe what you've done, provide evidence of value, and ask for votes.

Thanks! -@allancto

Ojimadu commented 6 years ago

Like allancto said, "I'd recommend editing the issue statement above with a full description of the work you did" as this meet up issue is quite technical and academic, I don't understand how participants would be able to contribute to the coop with the above topics or is this work more related to knowledge about RChain technology stack - Pi-calculus, Rho calculus etc.? If yes, then a grant or something similar to #755 would be suggested. Perhaps, more explanation would help me and others understand better. I have voted $1000 for this issue as it uses same materials from the #822. I'll vote percentages when I have a better clarity.

golovach-ivan commented 6 years ago

Why is RChain different from other blockchain technologies?

Casper concensus protocol and blockchain (sharding, namespaces, dag).
RhoLang smart contract formal verification (auditability, behavioral/spatial external type system).

What is RhoLang smart contract formal verification? It is writing liveness/safety/security properties (behavioral/spatial types) as Namespace Logic formulae and running tool that checks Smart Contract conforms/satisfy to a formulae.

But now it is impossible to do RhoLang formal verification.

There are only short list of academic papers and no tools, libraries or tutorials.

RhoCalculi is new and disparate process calculi. Namespace Logic is new and disparate modal/spatial logic. There are no tools on market for RhoLang formal verification. We must create them.

The goal of these meetups (#821, #822) - start a broad activity in next directions

RhoLang Formal Verification community - DOES NOT EXIST
Library of useful Namespace logic formulas - DOES NOT EXIST
Algorithm of formal verification for NamespaceLogic/RhoLang - DOES NOT EXIST
Formal verification tool (command-line and web interfaces) - DOES NOT EXIST
Tutorials/Manuals on Namespace Logic formulas - DOES NOT EXIST

This topic is academic and difficult. This topic like concensus protocol development. But we need to find a very small number of participants (with good Math/SC background) to develop core (algorithm, tool, library, tutorial).

Two meetups attracted 2.500 of viewers in one month. These are very good indicators for such sophisticated topic.

Please vote for this issue.

Ojimadu commented 6 years ago

Nice work. Well done.

dckc commented 6 years ago

I see reward were issued in the 201807 pay period.

rchain / bounties