buraq @burakemir@types.pl

@shriramk I think this is a nicer alternative

https://www.dhil.net/research/papers/thesis.pdf

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

Conways Game of Life on a Torus :)

@rntz @joomy @burakemir @maxsnew @shriramk I haven't been able to get Peter Van Roy's terse definition (in https://dl.acm.org/doi/pdf/10.1145/3386333) out of my head since reading it:

Meanwhile on Twitter:

@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 https://semantic-domain.blogspot.com/2013/07/what-declarative-languages-are.html

@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 *.

Is someone else using GPT-3 as a clever Google?

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?

@burakemir @joomy @shriramk

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

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

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

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 https://datenschutzkonferenz-online.de/media/dskb/2022_24_11_festlegung_MS365_zusammenfassung.pdf

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

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.

Militant decency.

#Gnu #TerryPratchett

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)