Bidirectional tools can often be used for unidirectional use cases, but they are also usually designed with those two specific languages in mind, which constrains the utility of the underlying bindings for work with other languages. You can’t use the bindings as a neutral “hub” that many languages radiate out from.

Too many programming languages researchers dismiss concrete syntax as an afterthought […] This received view ignores a critical factor: the human at the computer. Concrete syntax defines the principal interface through which programmers interact with the vast majority of programming languages. Moreover, this interface is hardly decoupled from semantics; even trivial-seeming differences in keywords, sigils, and indentation can affect how programmers utilize and reason about language behavior. Using examples from asynchronous control flow, gradual subtyping, first-class functions, and more, I will make a case for the importance of concrete syntax, why language designers often overlook it, and what this implies for those of us who care about the usability of abstractions. Finally, I will describe some preliminary work evaluating the role of lexical ambiguity in programmer comprehension of type system features.

A return to an old flame of mine.

see: https://slim.computer/concrete-syntax/

Some nice patterns, both in the main body and the comments, for implementing lenses with a light sprinkling of category theory.

via: https://haskellforall.com/2026/06/ergonomic-overrides-for-nixpkgs

What I enjoy most about these (semantic) editor combinators is that their use is type-directed and so doesn’t require much imagination. When I have the type of a complex value, and I want to edit some piece buried inside, I just read off the path in the containing type, on the way to the buried value.

via: https://haskellforall.com/2026/06/ergonomic-overrides-for-nixpkgs

Announcement post for the override-utils Nix package

A very compelling application of lenses!

Lookin’ at you, JSON

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure “all unsafe blocks are safe” can’t use the Rust compiler, you need a second tool like Miri. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.

A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.

“Hey, I have a good idea for a game,” I said. “It’s called the function machine game. I will think of a function machine. You tell me things to put into the function machine, and I will tell you what comes out. Then you have to guess what the function machine does.” He immediately liked this game and it has been a huge hit; he wants to play it all the time.

This post made me smile. :)

Overall verification resulted in a remarkably robust and rigorous codebase. AFL and Claude had a really hard time finding errors. But they did still find issues. Verification is only as strong as the questions you think to ask and the foundations you choose to trust.

Type inference challenges for real-world JSON

A case where bidirectional typing can be lightly cursed.

A post explaining why bidirectional type-checking is popular within the programming language theory community

via: https://haskellforall.com/2026/05/a-bidirectional-typechecking-puzzle

Keep Unwanted States Representable

Keep Unwanted States Representable

a declarative language is any language with a semantics has some nontrivial existential quantifiers in it

via: https://buttondown.com/hillelwayne/archive/people-get-confused-when-language-implementations/

Every escape hatch is a pit trap

PANE is a live, functional programming environment built around data-visibility. In PANE, all intermediate values are visible by default, and you construct a program by acting on these concrete values.