University/Notes
University/Notes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

vault backup: 2025-02-20 15:08:09

Browse Source
This commit is contained in:
Boyan 2025-02-20 15:08:09 +01:00
parent d62b2f8867
commit 680fb334ac
2 changed files with 10 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
.obsidian/workspace.json vendored
View File

@ -20,21 +20,8 @@
"icon": "lucide-file", "icon": "lucide-file",
"title": "Initial Questions" "title": "Initial Questions"
} }
},
{
"id": "846cc9fc78006404",
"type": "leaf",
"state": {
"type": "release-notes",
"state": {
"currentVersion": "1.8.7"
},
"icon": "lucide-book-up",
"title": "Release Notes 1.8.7"
} }
} ]
],
"currentTab": 1
} }
], ],
"direction": "vertical" "direction": "vertical"
@ -212,7 +199,7 @@
"omnisearch:Omnisearch": false "omnisearch:Omnisearch": false
} }
}, },
"active": "846cc9fc78006404", "active": "fcc28e70ad8acbd2",
"lastOpenFiles": [ "lastOpenFiles": [
"Software Engineering/TA Meeting 1.md", "Software Engineering/TA Meeting 1.md",
"Extracurricular/Misc/Plan.md", "Extracurricular/Misc/Plan.md",

9
Software Engineering/Initial Questions.md
View File

@ -7,12 +7,17 @@
- What is the expected level of background in Coq or formal methods? - What is the expected level of background in Coq or formal methods?
- Can you explain the process by which a smart contract's safety properties will be validated formally? - Can you explain the process by which a smart contract's safety properties will be validated formally?
- Are there any existing case studies or example proofs we might refer to for a better understanding of the expected output? - Are there any existing case studies or example proofs we might refer to for a better understanding of the expected output?
- How much of the formal verification process will be based on axioms versus fully constructive proofs?
- Define the contract verification criteria - Define the contract verification criteria
### Project scope clarifications ### Project scope clarifications
- Among the seven smart contracts being verified, which ones do you expect us to work on, and why those? - Among the seven smart contracts being verified, which ones do you expect us to work on, and why those?
- Which technologies are we going to be introduced to, if any? Will we have access to guides for Coq and Solidity? - Which technologies are we going to be introduced to, if any? Will we have access to guides for Coq and Solidity?
- How do you envision the high-level Coq framework integrating with existing Solidity projects? - How do you envision the high-level Coq framework integrating with existing Solidity projects?
### Optional
- How much of the formal verification process will be based on axioms versus fully constructive proofs?
- Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts? - Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts?
- "real numbers and integer approximations"? - "real numbers and integer approximations"?