Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution to our problems.

I don't want to discourage them from learning Iris, or designing a dependently typed language, but I really think that's missing the difficulty in formal verification.

I think the two areas that need focus are: ease of specification and automation. In short, we need to lower the cost of verifying a line of code, by at least an order of magnitude. These two objectives are also directly opposed to the direction Magmide sets as the goal. Ease of specification means we want to use the least amount of seperation logic possible, and hide it from the user if possible. Doing proofs / writing specs in seperation logic sucks and not for interesting reasons. Automation means favoring simpler logics, specifically we want to stick as much as possible to FOL since that's where we have good automation. By doing everything in a rich dependently typed language from the start it also makes it harder to do incremental verification, I think there is a lot of value in having a 'pyramid of trust' with more and more powerful tools which take you up a level of trust and verification, potentially requiring more input from engineers as they go up.

Finally, I think there's a lot of potential to explore in the interfaces we use to write, read, and debug proofs. I don't think tactic languages (as exist today) are the last word, and I think we should be doing a lot more interesting things to interface with and explore the proofs.