3 ms·

The Bosque Programming Language

72 points by RafelMri 3y ago

banashark 3y ago
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/overview.md https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...
greencore 3y ago
Apparently this project is now fully open sourced and developed outside Microsoft https://github.com/BosqueLanguage/BosqueCore/discussions/66#discussioncomment-6712178 https://github.com/BosqueLanguage/BosqueCore/discussions/66#...
msk-lywenn 3y ago
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.
- LudwigNagasena 3y ago
  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.
  - blixt 3y ago
    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).
    - LudwigNagasena 3y ago
      Oh, I missed the line with the `check` keyword and misinterpreted the comment I replied to. Yes, it is indeed very strange.
      - mark_marron 3y ago
        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.
damiankennedy 3y ago
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.
mark_marron 3y ago
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 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/research/papers/bosque.pdf https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...
- mb7733 3y ago
  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.
sshine 3y ago
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.
- mark_marron 3y ago
  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.
dalmo3 3y ago
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?

72 points by RafelMri 3y ago

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/overview.md https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...

greencore 3y ago

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

msk-lywenn 3y ago

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.

LudwigNagasena 3y ago
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.
- blixt 3y ago
  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).
  - LudwigNagasena 3y ago
    Oh, I missed the line with the `check` keyword and misinterpreted the comment I replied to. Yes, it is indeed very strange.
    - mark_marron 3y ago
      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.

damiankennedy 3y ago

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.

mark_marron 3y ago

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 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/research/papers/bosque.pdf https://github.com/BosqueLanguage/BosqueCore/blob/main/docs/...

mb7733 3y ago
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.

sshine 3y ago

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.

mark_marron 3y ago
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.

dalmo3 3y ago

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?