Yes, Kind2 will be a type layer on top of Bend, with a similar relationship as in JavaScript / TypeScript (but much more integrated, less ad-hoc and with proofs!). I don't want Kind2 to compete directly with Lean though, as it is doing an amazing job and I'm rooting for it. So, Kind2 will be just a type system for Bend that happens to let you prove theorems about your programs, rather than a higher promise to digitalize all of maths and stuff.