It is really a matter of what you want to prioritize. A language like F* is designed for provably correct software -- at the expense of requiring a full spec +

It is really a matter of what you want to prioritize. A language like F* is designed for provably correct software -- at the expense of requiring a full spec + working with the type system to complete any proofs that cannot be automated. Bosque takes a view that for most applications there isn't a complete specification to prove and instead aims to validate simpler assertions with a fully automated (even if sometimes incomplete) checker. In simpler cases, these systems may have similar feels but as the application gets larger then they will start to look very different in terms of developer effort (for proofs) and completeness of correctness guarantees.