lyxia boosted

one of my favorite, strangest websites is horg.com/horg/

it's an elaborate shitpost of a website that traces an imaginary taxonomy and phylogeny of little plastic waste products, particularly the little plastic bits that they use to keep bread bags closed (occlupanidae)

Dijkstra's notes (EWD879) that are quoted there are also a marvel in themselves. Like everything he ever wrote pretty much.

cs.utexas.edu/~EWD/transcripti

Show thread

I was looking into this after listening to a little story at the beginning of an ICFP19 talk by Wouter Swierstra, telling about Edsger W. Dijkstra telling about Martin-Löf telling about his type theory.

> He (Martin-Löf) was a very sympathetic speaker and convinced at least me (Dijkstra) that something (possibly even of great conceptual elegance) was going on. He spoke with an endearing care.

m.youtube.com/watch?v=iU7UtoM7

Show thread

The Curry-Howard correspondence is often brought up as a relation between proving and programming, but at least Martin-Löf actually attributes the connection to programming to Kolmogorov. Whereas today types are easily associated with programming, Martin-Löf presents the connection in the order Types-Proposition-Problems (whose "solutions" are programs), that's kinda surprising today. Read his seminal paper, Constructive mathematics and computer programming.

cs.tufts.edu/~nr/cs257/archive

Determinization is a in the of state machines and simulations. I'm not sure whether it's a profound or trivial fact.

Also, it's crazy how the slides draw themselves when I know everything I'm going to say first.

Show thread

Practice talk round 1: it's good, but change everything to make it better.

lyxia boosted
lyxia boosted

My paper's on arXiv
arxiv.org/abs/1912.05601
It was rejected from CPP so I can't say anything fancy like "it's gonna be published at so-and-so!" or whatever but here it is!

lyxia boosted
lyxia boosted
lyxia boosted
lyxia boosted
lyxia boosted
lyxia boosted
lyxia boosted

Metamorphic testing is a method for finding properties of functions amenable to automated testing: find simple relations between inputs that map to simple relations between outputs. It's a simple but powerful idea around which to structure testing.

hillelwayne.com/post/metamorph

In , types and propositions, programs and proofs, all use the same syntax. But proving a proposition and implementing a program are still different activities. We can give orders or recite poetry in English, but are orders and poems the same because they share the same language, sometimes even the same sentences?

lyxia boosted
Show more
niu.moe

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !