Meetup: Formal Verification aproaches for RhoLang

golovach-ivan commented 5 years ago

Hold Meetup: Formal Verification aproaches for RhoLang (Europe/Ukraine). Explain and compare 5 different ways

Interactive Theorem Provers (write the specification as an independent mathematical theorem).
Contracts (encode the specification as assertions, pre/post conditions).
Barbed Bisimulation (write the specification as an simplified program in the same language).
Modal/Separation Logics (encode the specification as logic formulae).
Kobayashi Type Systems for Process Calculi (encode the specification into channels types).

This issue is result of #945 research activity.

Benefit to RChain

grow Russian-speaking community
develop slides for "meetup in a box" project (#779)
publishing video on youtube channel for 25.000+ developers

Budget and Objective

Involved

golovach.ivan - 75% kovmargo - 25%

Expenses

Publicity, Banners, Digital graphics $100 Hall renting $100 Camera and associated gadgets renting + video processing $150 Logistics $50 Slides development - golovach.ivan time Speech/Info preparing - golovach.ivan time Video processing consultancy, organization - kov.margo time

Estimated Budget of Task: $[2000] Estimated Timeline Required to Complete the Task: [1week] How will we measure completion? [processed video uploaded to Youtube channel + slides uploaded to #779 ("meetup in the box" issue) google directory

Ojimadu commented 5 years ago

@golovach-ivan, Have you gotten any sponsor for this? If No, please don't proceed until someone from the marketing organization supports this with a budget.

dhsorens commented 5 years ago

@golovach-ivan A reference book is under way in the rchain/Rholang directory. I would be very interested in getting involved in anything that happens here, as I am building the formal semantics of Rholang for precisely this purpose. Feel free to contact me on discord at @ Derek.

rchain / bounties