CIP-0145? | Structured Contracts #963
Conversation
rphair
changed the title
There was a problem hiding this comment.
@polinavino I think this is a fine place for this to be, since we have a good target audience here to identify with potential usage & implementations - will tag some contributors to similar proposals that I can think of below & you are welcome to invite some more.
The Triage tag will put it up for introduction, rather than review, at the next CIP meeting: https://hackmd.io/@cip-editors/104 - so if you still want to incubate the idea before then you can put it in Draft review status before then. Otherwise I will try to keep it in the limelight to see if other voices can start building it up a bit... which generally doesn't happen if Draft status keeps it off the active proposal lists.
If it remains on the boards the editors will have to submit another review for compliance with the CIP-0001 document structure: unless you choose to attend to it in due course along with the validation of this idea & community participation.
rphair
added
State: Triage
|
@rphair I would he happy to attend the next Triage meeting to introduce the PR. Do i need to fill out any document? Get an invite link? |
polinavino
changed the title
|
@polinavino we will always be happy to have you there & every meeting is open to the public. Invite link (https://discord.gg/J8sGdCuKhs) and some other CIP-related info (especially the pages on review) you may find interesting are on the Wiki for this repo: https://github.com/cardano-foundation/CIPs/wiki |
There was a problem hiding this comment.
Structural review promised in #963 (comment) (I'm not qualified to review the subject matter itself).
|
@polinavino we've chosen (at today's CIP meeting) to leave this tagged Until then we don't have grounds for either Personally, I might be in favour of progressing it anyway if a more detailed Path to Active could be developed that would leave the community with a path to follow if this were merged without such confirmation. |
|
@rphair I was planning to come to the next meeting, thinking a link to it would be posted at https://lu.ma/cardano-cip whenever it is scheduled. There were no meetings there for this week. Is that the wrong place to look for a link to register for the meeting? |
|
@polinavino the primary source for the meetings is at the top of the CIP Discord server menu under I only found today that Luma doesn't have the 2025 meetings yet. Maybe the sequence stopped when the 24 December meeting was cancelled, or maybe the meetings hadn't been repeated into year 2025. @Crypto2099 set that up & I think he will be following up about it. I am very sorry to have missed you. The meetings on Luma and Discord have been mutually consistent for as long as I can remember. Of course we will be happy to have you at the next meeting & hope to see plenty of activity in this thread in the meantime. |
|
@rphair Thank you for the link! I am sad to have missed it - too bad Luma was being weird, I should have looked harder on Discord. I will try to make it to the next one 😅 |
rphair
changed the title
There was a problem hiding this comment.
Thanks @polinavino for the introduction at the CIP meeting today. Please rename the project directory to CIP-0145 and update the link to your proposal in the first comment above. 🎉
Editors & community agreed this idea should be circulated, that it is a sound and useful proposal, and that giving it a number will help with the specialist review that it needs to identify specific applications & confirm an implementation path.
We thought a further way to tag qualified reviewers might also be through AGDA speciality: although we understand these specialists are generally pretty busy with their own work. @WhatisRT @lehins @bwbush (Ledger + Consensus) would you have any ideas who might be interested in applying this and/or giving it a practical review?
| as an instance of our proposed framework, including anything from minting policies, to a basic (single-execution) | ||
| UTxO-locking script, to sophisticated stateful apps distributed across multiple UTxOs and scripts. We do not propose any | ||
| automation for defining structured contract instances, however, the scope of this CIP should include automated conversion | ||
| from completed Agda smart contract functions to Plutus code. |
There was a problem hiding this comment.
I'm skeptical that automated conversion can produce both readable and performant plutus code. It seems more feasible to use it as a reference implementation.
There was a problem hiding this comment.
Well, technically you could use agda2hs which should generate Haskell code that isn't different from hand-written code. In many cases that can probably be quite performant. But agda2hs has its own set of constraints on the Agda you can write, which gets in the way of having the proofs you want. So yeah, it's probably more realistic to have hand-written scripts.
There was a problem hiding this comment.
Maybe i should rephrase that as "looking into automation is a possible next step for the project if/when it gets traction and has working examples", and suggest agda2hs as an approach to consider.
|
I don't know anyone outside of IOG who really uses (hard) formal methods on Cardano, maybe the RV folks do some of it? I think inside of IOG most people who do FM are already familiar with this work to some degree. So sorry, I don't have any concrete suggestion. |
I wrote up a CIP for structured contracts before it gets forgotten entirely. It is mostly to try to bring some visibility to the project and find out if anyone is interested in using it to verify their contracts. The gist is that the "structured contract formalism" is easy to define (and basically done), but the difficult part is implementing some (all?) of the examples discussed there.
Any feedback is welcome - including opinions of whether or not, and how, I/we should try to pursue this further.
(rendered proposal)