The Bosque Programming Language | Hacker News Reader

The Bosque Programming Language

microsoft.com

72 pointsRafelMri13 comments

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

Very interesting ideas -- all the way the small practical stuff like being able to expose symbols only for testing without making them public, up to the more ambitious stuff about validation and constraint checking. As a broad research language the pitch is probably not focused enough to draw in users that happen across the docs, but I doubt mass adoption is the goal at this point!

I would love to use a language that implemented even just the "simple" parts, and I doubt I would be the only one.

One specific suggestion I have about the overview and docs is that I think the language around "Cloud" and "Restful/API computing" is more specific than it needs to be. While features like the APITypes would definitely be most useful for cloud/web software, I think the same ideas could be very useful for any kind of software. Anything that even writes a JSON config file could benefit from that concept if I understand it correctly.

Apparently this project is now fully open sourced and developed outside Microsoft https://github.com/BosqueLanguage/BosqueCore/discussions/66#...

Shouldn't the 8th line of the example code read "requires release (op == CalcOp::add || op == CalcOp::sub) ==> arg 2 != none;" ? I'm assuming it's some kind of constraint. Although if it is, the following "check arg2 != none;" seems redundant.

Yeah, the second `CalcOp::add` should be replaced with `CalcOp::sub`, but `arg2 != none` is not redundant. The condition narrows `arg2` from `Int?` to `Int` when `CalcOp` requires two arguments.

EDIT: Oops, I misread the comment. The following the following "check arg2 != none;" indeed seems redundant.

Since the example leads with:

> Many features that make the Bosque IR amenable for automated reasoning involve simplifying and removing sources of irregularity in the semantics.

I do find it strange that it both shows a bug in the logic which causes an irregularity, but also that this irregularity is allowed because of the need of a second check, rather than failing to compile because the type would be narrowed by the initial constraint (if the op argument is add/sub then arg2 MUST be non-none).

Oh, I missed the line with the `check` keyword and misinterpreted the comment I replied to. Yes, it is indeed very strange.

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.

Very interesting, so this is another potential for Typescript-like -> Native code.

The feature set looks pretty neat, and it's probably the first project by a larger company that I've seen use deno (required for building).

Docs are pretty light, but there is _some_ here: https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...

Is the requires release... line correct e.g.should it be add or sub?

Also, there is the additional check... line which seems to imply the same thing.

I buy the premise described, but I don't understand the example given.

The example (disregarding the small errors) resembles constraints from Liquid Haskell / F*...

So there must be something I don't get.

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.

Could someone ELI5 what makes that sample code good?

I have no context about intermediate representation or regularised programming languages.

Is it about speed, size, safety? Does it enable automatic proving?

Reply on news.ycombinator.com