Pinned toot

Announcement: here is something I worked on for a while - a language extending Datalog. It also does something that resembles type-checking. github.com/google/mangle

GitHub discussions look nifty. I will give it a try and ignore my worries about moderation load. What could possibly go wrong.

buraq boosted

@shriramk I think this is a nicer alternative

dhil.net/research/papers/thesi

Keep the usual API, but use effect handlers to hand out fine-grained permissions if desired.

buraq boosted
buraq boosted
buraq boosted
buraq boosted

@joomy @burakemir @maxsnew @shriramk I dislike the use of "backtracking" for this: it confuses specification & implementation. You can implement logic programming / regexes with no backtracking (eg. by translation to DFA). cf semantic-domain.blogspot.com/2

buraq boosted

@burakemir @shriramk @joomy

This is not a shitpost thank you.

A regexp is a logical formula with denotation in a set of "non standard truth values": the poset of predicates on strings rather than classical truth values {top, bot}. Empty and alternatives denote the bottom element and the join of this poset. Regular languages are closed under intersection so it is ok to add in conjunction as well. Kleene star is a particular LFP. The characters are atomic formulae and the empty string/sequencing are interpreted as a nice monoidal structure of the poset of languages (Day convolution).

A different way to say this is that regular expressions can all be interpreted as formulae in a non-symmetric variant of the logic of bunched implications where the sequencing is the *.

buraq boosted

TIL json with commas and comments JWCC. nigeltao.github.io/blog/2021/j

Good reminder of why JSON is an objectively bad specification. Also note the stylistic adherence to the literary genre AB form where A "rant that there are too many extensions" followed by B "here is our extension"

buraq boosted

I recently learnt that abstract machine (such as Krivine's abstract machine or CEK machine) can be derived instead of invented. But, what is the implication on the logical side, then?

buraq boosted

@burakemir @joomy @shriramk

I would say it as functional programs are terms, logic/relational programs are types.

buraq boosted

How much public space we've surrendered to cars (Swedish artist Karl Jilg)

buraq boosted

@burakemir @maxsnew @shriramk has something weird to do with distributive categories and closures. Having distributivity or full exponential objects (function closures) is incompatible with coexponential objects which are weird but you can think of as nonlocal control flow basically.

If you don't have functions or nonlocal control flow (so something like the Kappa calculus) programs can be evaluated backwards as well as forwards.

buraq boosted

German data protection authorities find that Microsoft 365 cannot legally be used for personal data (especially in public sector, e.g. schools) due to lack of end-to-end encryption, giving US intelligence agencies excessive access to personal data datenschutzkonferenz-online.de

Looks like the GitHub repo got 400+ ⭐​ ... in one weekend? I like this open source thing.

buraq boosted

i might have my criticisms of mastodon, but the founder of post is out here pretending “net worth” is a protected category to signal you can’t make fun of billionaires on his a16z-funded twitter alternative

buraq boosted

It seems no matter where I go, I find myself wishing that companies would employ (engineering) historians.

Someone who would interview employees and read docs and then write chapters about each major component of a company and how it got to be the way it did.

buraq boosted
buraq boosted

I'm working with an organization that may eventually fund proposals to fund workshops for research groups working on "mathematics for humanity". This would include math related to climate change, democracy, economics, health, maybe AI risks, etc.

I can't give details until it solidifies.

However, it would help me to know a bunch of possible good proposals. Can you help me imagine some?

A good proposal needs three things:

(1/n)

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.