mark_marron

Hmm, that is an unfortunate typo and I don't have access to the page any longer to fix it :(

This example is from an earlier version of the language that was experimenting with aggressive flow sensitive typing. Interestingly, I came to the conclusion that, while sometimes magically nice, it was also often confusing. So, in the version that is (slowly) getting built as the first _release_ version has a simpler and more explicit algorithm.

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.

Hi, this is Mark, the lead researcher and developer on the project. Cool to see it on HN today. Happy to answer any questions!

As a bit of an update, this project is not at Microsoft Research anymore. The new (main) repository is at https://github.com/BosqueLanguage/BosqueCore. MSR was a great place to work and do the initial work on this project, but was not the right place to make this a fully free and open language for real users.

Progress was a but slow in the last year while I found a new home but I am very excited to be starting as a professor at the University of Kentucy in January where Bosque will be the main project for my group! There is a paper from earlier this year that describes the language design, based on our experiments over the last few years, and shows some results from prototype tools built on the language. The Intro and Section 7 are pretty good for a quick overview of things: https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...