> 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 mention

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