Show more
lyxia boosted
lyxia boosted

A sample of type-driven programming with dependently types.

Programming totally with head and tail

blog.poisson.chat/posts/2020-0

lyxia boosted

I wanted to procrastinate a little by playing with hs-to-coq. Now I can't stop because I started writing a tutorial and somehow a point I was not trying to make turned into yet another tutorial on dependent types...

Praise Obj.magic! It keeps bailing me out of Coq extraction problems.

lyxia boosted
lyxia boosted

Oh shit, I've been using an unreleased version of coq-printf for so long, I forgot the next version adds a MAJOR feature (scanf) and I just bumped the version from 1.0.0 to 1.0.1 😱

Sweet drama around The Study on the effect of programming languages on software defects.

This is How Science Happens • Hillel Wayne

hillelwayne.com/post/this-is-h

lyxia boosted

I figured out a name for my #Gopher client I wrote in #Haskell... "Waffle!"

Both "gopher" and "waffle" in French is "gaufre:"

"The origin of the word 'gopher' is uncertain; French gaufre, meaning 'waffle', has been suggested, on account of the gopher tunnels resembling the honeycomb-like pattern of holes in a waffle…"
—"Gopher," Wikipedia.

I only have a few things left before the first release!

github.com/hyperreal-gopher/wa

#GopherProtocol

lyxia boosted

An Inconvenient Truth: The Curry-Howard Perspective. That has to be a great joke paper. 4/4

Show thread

Hot take: general recursion has something to do with global warming. 3/

Show thread

A connection is thus to be drawn between recursion and feedback loops of certain physical systems. 2/

Show thread

Notions of loops in various domains are unified under abstractions like traced monoidal categories. 1/

lyxia boosted

Rain drops from the sky, grave and cloudy,
falls on the walls, damp and gloomy,
coats the windows with drum and clatter,
storms the streets in a tantrum and a roar,
showers away the dirt and the spirits,
bows to the bearer of warmth and light.

Show more
La Quadrature du Net - Mastodon - Media Fédéré

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!