[thethirdone]

> To throw another one onto the _have you looked at X_ pile,

I am pretty sure I have seen Dafny before, but it wasn't on the top of my head. Thanks for mentioning it.

> I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting.

I agree with both of those statements. I am not thinking of something revolutionary. I have been thinking of a few ways to make it more ergonomic than Dafny though. Refinement types would be one of the key ways to do that.

I think all of the key capabilities would be the same though. It would probably make sense to make a transpiler to Dafny to try it out.