@kha @mattam @beta We just don't solve these kind of equations in Agda. Here's the example with the error in comment: gist.github.com/jespercockx/fc

I suppose it takes a different style of coding, but I don't hear Agda complain about it too often (but perhaps the people who would complain are all using Coq or Lean instead).

We do have a (relatively recent) option --lossy-unification which enables a first-order unification heuristic (and makes the example pass) that some people seem to like, so there is definitely more work to be done.

In one day - one day! - of going open source, the Typst typesetting system passed 5,000 stars on Github.

If you ever needed evidence that there is a real hunger for a TeX replacement, this is it.


@jonmsterling Wow, congratulations! You should tell me one day the trick to skipping the assistant professor step ;)

I'm overjoyed to announce that I will be starting as an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge this fall!

@jonmsterling i think the human brain can only take so much type theory before it needs a day off to nap or something

*Red Team Blues* is my next novel, a #PostCyberpunk anti-finance finance #thriller; it's a major title for my publishers Tor Books and Head of Zeus, and it's swept the trade press with starred reviews all 'round. Despite all that, #Audible will not sell the #audiobook. In fact, Audible won't sell *any* of my audiobooks. Instead, I have to independently produce them and sell them through Kickstarter:



I'm too tired just now to tell you what little I know about the beginnings of an answer to this question but...

Orbits. What are orbits? Never mind what groups are or how they act on whatever they act on: what are the orbits? What is it to be a system of orbits and stabilisers that comes from a group acting on a set?

I feel like Ptolemy having a go at Copernicus in 2023.

Certified logic-based explainable AI (The case of monotonic classifiers). ~ Aurélie Hurault & Joao Marques-Silva. hal.science/hal-04031193/docum #ITP #Coq #XAI

Daniel J. Velleman has translated parts of his classic text "How to prove it" into Lean 4!


"How to prove it in Lean" goes through examples in the original book, and discusses how they can be proved in Lean. He also talks about how Lean's use of type theory rather than set theory affects this kind of basic mathematics, and furthermore gives clear installation instructions for anyone who wants to play along at home!

TU Delft already has a separate department of Intelligent Systems, and will soon have a separate master on Data Science and Artificial Intelligence Technology. But this does not seem to prevent AI research from also happening elsewhere.

Proudly helping to avert the AI apocalypse by proposing student projects, thus enabling smart students to spend their brain cycles on building type systems instead of AI models.

(This toot brought to you by several students telling me they found one of my proposals by searching for anything that did not have "AI" or "machine learning" in the description.)

@beta @mattam This is especially true because the issue disproportionately affects *invalid* programs, e.g. during editing. Which, yes, we do not have a good database of either.

@ionchy This feels like part one of a meme where the second part involves you saying "Oh no" while being crunched under a huge pile of eta-expanded terms.

Got access to Google Bard! I'm pleased to report that it is ethically opposed to necromancy

The Proceedings of EVCS – the Eelco Visser Commemorative Symposium – have now been published online, open access:


@beta I'm not sure I see what it means to "note how arguments are used within the function". Could you give an example where Coq or Lean or Agda could be smarter?

@mattam @beta @kha Configurable levels of abstraction are coming to an Agda near you Soon (TM): github.com/agda/agda/pull/6354

I was a happier man before I knew that Coq and Lean unification is inherently exponential (and practically significantly so, especially on failure) because of backtracking

Excerpts from §2 of @beta & @mattam: A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading

@mattam @beta @kha The problem here is not unification per se but rather backtracking. It is possible to implement a unification algorithm that only makes forced steps so it never needs to backtrack, and still have a usable system.

Show older

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