l'empathie mécanique @dpwiz@qoto.org

@jesper wide.

("none", even, if a dependency is on Stackage)

It's cheaper to pin down version than to fuss around allow-newer.

@tristanC They aren't migrating if I understood correctly. Just need a way to produce TS apps from Agda sources and LLM translation happens to do a better job at it than a "real" compiler.

2022: We need end-to-end certified compilation!
2024: Nah, just stuff your "proofs" into an LLM to get "executables".

https://x.com/VictorTaelin/status/1837925011187027994

> Since the AgdaJS compiler isn't maintained, and since creating one would be a $1m-budget project, we're now compiling 590 Agda files to TypeScript using Sonnet-3.5, to let us run our apps on the browser.

> The results are excellent. Almost all files work with no intervention. Error rate is lower than the current AgdaJS compiler, on which we found bugs. Performance is 20x higher. We're now automating this in a loop.

Literate programming soon be like:

> Once upon a time, there was a little file..... [TAB] .... And they lived happily ever after.

@bascule Unfortunately the numbers don't add up and we're about to get our collective geese pretty damn cooked. I hope we'd survive and avoid collapse, but the situation looks "too little, too late" dire.

@6d03 ... in the darkness >>= them
In the Land of Mordor where the types lie.

@someodd It looks... reasonable? You can shuffle a few calls here and there, but it's just a few lines of code.

@evacide Call your republican representative too (if you happen to have one).

@cerberus1746 @acegikmo Y down

@omgubuntu Respect for not leaving the issue even after so much time.
Some repos have autoclose policies and this is so fucking annoying!

Anything is a cipher if you're brave enough.

@TheIneQuation @feyter @aras Skill issue.

@6d03 Can it be used for bootstrapping GHC?

From the cult classic "2024":

> The Resistance has always been at war with the Establishment.

@david_chisnall I talk about what I've seen first-hand. Early models were indeed shit to the point of being useless.
The original GPT was barely coherent. GPT-2 required a prompt choke-full of examples and boatload of crutches to keep its shit together. GPT-3 (and LLAMA-2) still requires non-trivial amount of guidance but it starts getting somewhere (41% of correct summaries measured in there is no joke! You can guesstimate how many orders of magnitude it is above the random guessing. Spoiler: a fucking lot, given the recursive dimensionality of language.)
I don't have the numbers for 4-gen models, but I've checked the pubs before replying and some report a problem in benchmarking summaries as the score difference wrt humans is difficult to raise above the noise.

@david_chisnall Eh.. For the same reason it does *anything at all*?
I think the silliest of them all, the hand-written numbers recognition models, already does learn the "nuance" and inter-relationship between the pixel values while discarding the noise and unimportant variations.
What exactly is the "context" problem you think is intractable if not that?

@alan Try better model. Claude can give pretty good *explanations* and not just "greater than five" like Gemini (and open-weights crap) does.

@david_chisnall I'm surprised by your claim. Of course summarization is one of the training disciplines, so the models should be good at it. And the growing demand would drive more resources into it and the state of the art would be even better.

And the linked post is misleading. Testing (and even reporting) LLAMA-2 level models in mid 2024 as "most promising" is... meh. The title should be extended with "... in mice".

@tante Nah, it's just a regurgitation of ancient (by now) talking points. Nothing new in there.