A path to a verified HVM · HigherOrderCO/HVM2 · Discussion #120

rigille
May 19, 2022

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

Interaction nets in Coq
- Prove preservation of semantics given cloning limitations
- Prove complexity bounds
- Prove strong confluence
Interaction nets in C

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

Replies: 5 comments 5 replies

o-santi
May 19, 2022

This sounds like a splendid idea! Let's do this.

0 replies

zicklag
Nov 19, 2022

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?

0 replies

VictorTaelin
Nov 19, 2022
Maintainer

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.

3 replies

@zicklag

zicklag Nov 19, 2022

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.

@rigille

rigille Nov 23, 2022
Author

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

@zicklag

zicklag Nov 23, 2022

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. :)

zicklag
Nov 24, 2022

Read Software Foundations and you're good to go.

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.