one of my favorite, strangest websites is https://www.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.
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.
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.
Also, it's crazy how the slides draw themselves when I know everything I'm going to say first.
I don't believe in non-constructive logics: https://tooot.im/@Calvinn_Hobbes/103314126118723981 I am a classical atheist? 🤔
My paper's on arXiv
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!
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.
In #Coq, 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?