Meetup: Formal Verification aproaches for RhoLang

[golovach-ivan]

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]

@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]

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