mrkmarron

What is your take on usability of these systems? In practice they seem to be rather un-ergonomic and usage devolves into require everything.

As agentic systems seem to mainly interoperate with REST style systems I suspect that using URIs for resource use descriptions would be more natural.

The key capability that Bosque has for API specs is the ability to provide pre/post conditions with arbitrary expressions. This is particularly useful once you can do temporal conditions involving other API calls (as discussed in the blog post and part of the 2.0 push).

Bosque also has a number of other niceties[0] -- like ReDOS free pattern regex checking, newtype support for primitives, support for more primitives than JSON (RAML) such as Char vs. Unicode strings, UUIDs, and ensures unambiguous (parsable) representations.

Also the spec and implementation are very much not proprietary. Everything is MIT licensed and is being developed in the open by our group at the U. of Kentucky.

[0] https://dl.acm.org/doi/pdf/10.1145/3689492.3690054

That is a key item that we are working on addressing in the 2.0 milestone for Bosque[0]. The goal is to build a language and system model that allows us to reliably sandbox and support agents in constructing "Trustworthy-by-Construction AI Agents."

This addresses both accidental misbehaviors and targeted prompt (or other) attacks on agents -- for example ensuring that an agent will never misuse a payment API or return that an order succeeds without really placing it!

[0] -- https://bosquelanguage.github.io/2025/09/26/trustworthy-agen...

Just saw the edit. I have 2 answers:

1) Fuzzing is under-utilized even for simple code. AFL is dead easy to use and, even so, most projects don't have it in CI runs. So, despite how much I like it, in general it seems people do not see value in this type of testing.

2) The effort to handle external state (say a restful call to get stock ticker info) needs to be mocked -- which is deeply unpopular -- or handled by record/replay which works ok-ish but eventually breaks down with divergences. Outside of well-chosen domains it these eventually pop-up and add an additional pain point that builds on item 1.

At the end of the day you have 2 problems (1) how to make execution deterministic within some boundary be it a process, hypervisor, or distributed system and (2) how you handle non-determinism when data crosses this boundary. You can move the boundaries and effort around but the problems always exist. So, if you are claiming that you have a sweet spot on this tradeoff then I could certainly believe that, if you claim that you eliminated this boundary issue then I am highly credulous.

I'll agree with you on indeterminate behaviors though, I suspect they will eventually be seen like the "billion dollar" mistake of null pointers.

I just rewatched the end of the video to make sure I didn't miss anything. Deterministic execution and replay is very-very well-known and understood. It is possible that your packaging and market fit is right on. Lots of cottage industry in DB testing and bug finding -- but not clear how this generalizes and why something like Coyote [1] (to pick one) wouldn't work as well.

So, fuzzing has been applied to very stateful and very large industrial systems for some time. And yes it is very cool but I feel like I am seeing more "sizzle than steak" so to speak. Great engineering though, hypervisor work is very challenging.

[1] https://www.microsoft.com/en-us/research/blog/coyote-making-...

Thanks for sharing, I felt like there were earlier but the x,y trick jumped out at me and that was the one I remembered off the top of my head.

I think you underestimate the level to which this area has been studied. And I wish you would talk about these new results then instead of announcing 5+ year old results then.

It would be great to see progress in this area (not my primary area of work BTW) but I am not seeing anything here, technically, that is going to make that happen -- maybe it is just getting all the parts in place and magic happens. It just makes me scratch my head a bit.

FYI playing Super Mario with fuzzing (AFL) was done in a fun 2020 S&P paper. Also finds bugs and security issues.

"IJON: Exploring Deep State Spaces via Fuzzing" https://casa.rub.de/fileadmin/img/Publikationen_PDFs/2020_IJ...

The design of the language is done in a manner that allows us to translate the code (and all conditions) into very friendly SMTLib code -- that we don't need to add a lot of additional checks like frame rules or havocs and where the set of theories (and their combinations) are well behaved.

We have some info on this in the research papers section and documents but are planning on a full paper focused on how this is done (particularly in the presence of union types, dynamic records/tuples, etc.)

Hi and thanks for the questions:

1. By design the language provides some novel memory invariants including, no cycles in the object graph, no old-to-new pointers, and no pointer updates. Thus, we don't need to worry about cycle collection, can greatly reduce the number of Ref-Count operations, and can (later) employ pool allocation more consistently.

2. Bosque also supports by-value types (including the future ability to do by-value unions) and, since the language is referentially transparent, the compiler can aggressively use stack allocation and copy semantics. Also, the collections are all fully determinized and use low-variance implementations to avoid "bad luck" performance anomalies.

3. The compiler does not enforce the checks. They can either be checked at runtime or checked by converting the program into a logical form that Z3 or another theorem prover can check. Values in the language are immutable and there is no concurrency (yet) but since the language is immutable concurrency is by definition data-race free.

You are right, allof is inconsistent with the language naming conventions. I was updating some other collections support and made that fix as well. Thanks!

Hi, project owner here, great to see this on HN and always happy to hear from folks here and on the GitHub repo.

We also have a webinar with Q&A scheduled for Thursday morning (https://note.microsoft.com/MSR-Webinar-Programming-Languages...) which may be of interest as well.

There were some discussions for a more general system -- e.g. Int[Seconds] would be a typed int indicating the contents represented seconds.

We needed to think more about all of these usecases and how things worked so we decided to start with just strings as the most useful. It is great to see you had the same idea though and would definitely like to revisit this in the future.

My understanding it Elm checks for signature changes such as adding a parameter to a function. We would like to do more and actually compare the actual behavior of the code before/after the change as well.

Great question. We take a very maximalist stance here and do not provide any environmental API’s in the Bosque language. Instead all IO, data-time, IP address operations must be part of a host platform – similar to how JavaScript does not provide IO or an event loop in the spec but relies on the browser or Node.js to provide it.

With this model the host can just log/record the environment interactions. The details of this host and integration are an open issue, both research and engineering, but I am very excited by the AMBROSIA architecture (https://github.com/Microsoft/AMBROSIA) by one of my colleagues as a possible design.

The current purpose is explore language design choices and their impact on their general utility for programmers and enabling automated developer tools (like verifiers and compilers). The hope is to use Bosque as a proof of concept for various ideas.

Some examples of better than existing languages are included as case studies in section 5 of the technical report:

-Automatically finding (ideally) any runtime error and producing a test case for it.

-Verifying that a SemVer update is safe or flagging where it will change the behavior of your code.

-Supporting compilation to high speed SIMD code or other accelerator architectures.

This is all still an aspirational goal and a lot of work remains though.

It is a Spanish word used in the SouthWest US for forest along a river. No particular reason behind the name, just a unique and easily searchable choice.

I would say accidental complexity comes from mostly historical reasons. Two sources discussed in the report are reference equality and looping. These make a ton of sense if you are implementing a language with a compiler that targets an x86 processor. They map naturally to the features of the hardware but make other tasks impractical, e.g. compilation to a FPGA or verifying a SemVer dependency update doesn’t break your application.

Section 5 of the paper explores some scenarios that, once this “accidental complexity” has been removed, become much more feasible. These types of experiences are currently aspirational, and much work remains, but the hope is to demonstrate the practicality and value of these concepts.

Hi project owner (Mark) here. It is a bit late in the evening for me but I will try to answer any questions when I can.

The Bosque language is currently in a very early state with lots of work to do and not ready for practical use. However, I am very excited by the potential in the concepts and wanted to make the project a collaborative endeavor, including both other academics and developer community, from the start. At this point the goal is to explore interesting options in the language design space – whether the Bosque language becomes mainstream or just provides useful ideas for other languages to adopt. So, please take a look, expect plenty of rough edges, and we would love comments, suggestions, and PR’s on the GitHub repo.