Replies: 5 comments 5 replies
-
|
This sounds like a splendid idea! Let's do this. |
Beta Was this translation helpful? Give feedback.
-
|
I'm curious, is Kind2 mature enough to use for our proofs instead of Coq, or is that still too new or not have the features we need? |
Beta Was this translation helpful? Give feedback.
-
|
What features you need? Kind still lacks some features that are important for serious mathematics, namely coverage/totality checking. You can use it to make any kind of formal proof you would on Coq, and it would be much more pleasing to work with (specially given how fast the checker is), but you'd need to make sure you don't write loops. Also, if you're a fan of tactics proving style, Kind doesn't have that. And it won't prove anything for you via complex unification, so you can't just skip impossible cases (like on Agda), you must write the proof explicitly, but I actually prefer it that way. All in all, there are differences that make it worse or better. It really depends on what you need to do. |
Beta Was this translation helpful? Give feedback.
-
|
I'm actually not sure what features we'd need. I just heard about abstract mathamatics and formal proofs by finding Metamath 5 days ago and now I'm quite interested in finding practical applications of proofs and learning how to make them. I doubt I'll be able to make any progress on this myself ( yet ), but it seemed like if we were going to verify the HVM then it'd be great to do it with Kind of possible. |
Beta Was this translation helpful? Give feedback.
-
|
I prefer Kind2 and Agda to Coq from a pure language design perspective. However Coq has the biggest ecosystem of proofs. There's a lib for concurrent separation logic compatible with a verified compiler, another lib of concurrent separation logic that'll likely be compatible with Rust soon, lib for reasoning about distributed systems — which is something I would like tackle as well —, libs with theorems about permutation groups — which arise when we compose wirings —, and also more learning material to learn all of that. Using previous work this project is more likely to succeed |
Beta Was this translation helpful? Give feedback.
-
|
An excellent point! From a little looking around it definitely looks like coq has one of the largest ecosystems for formal proofs, which is very cool. I'm not sure how much time I'll find to actually work on verifying HVM or not, but I'll start reading Software Foundations and see what happens. :) |
Beta Was this translation helpful? Give feedback.
-
I just wanted to shout out an extra thanks for pointing me to that course @rigille. I've gotten to the end of the first chapter, and it's pretty awesome! This is exactly the kind of thing I was looking around for, coincidentally enough, not even related directly to HVM initially. 🤩 Coq actually seems quite nice as a proof environment so far. I'm using the VSCode plugin and the workflow seems pretty enjoyable at least while going through the first chapter. |
Beta Was this translation helpful? Give feedback.
-
|
I've been wanting to study it for a while. I really hope I can find the time to do this. 😅 |
Beta Was this translation helpful? Give feedback.
-
|
It's addictive isn't it? 😄 |
Beta Was this translation helpful? Give feedback.
-
|
It would indeed be nice to have a formal verification of the HVM. (Especially the variant that will be used in Kindelia for smart-contract execution.) |
Beta Was this translation helpful? Give feedback.
-
HVM is well on its way to becoming the fastest functional runtime. Could it also become the most reliable functional runtime? After looking around in the current verification engineering ecosystem I think it can. My idea is to first define interaction nets in Coq, then define @VictorTaelin's memory model in C and prove that it's safe and preserves the semantics of inets even considering concurrent reduction of terms and other optimizations. So the roadmap sketch is
But is certain that more things will show up as we go. Would you like to help? Share you ideas. Read Software Foundations and you're good to go. We start after two people show interest. 😁
Beta Was this translation helpful? Give feedback.
All reactions