I did the #daily#CavesOfQud build. Died horribly (this is the way) quite proud of what I achieved though. It was a fun break from reality. exploring a procedurally generated high tech-low-life fantasy swamp. Love me a good chrome revolver and salve injector.
I did not tell my father I was leaving. I hadn’t told him much for years. I took his sword, his chainmail, his buckler. I laced my boots–a gift from my mother. I marched. Down the long road. Through the dark forest. Over the high mountains. Trudging through salt marshes.
I sucked buttons because I was thirsty, and without water. I slashed at crocodiles. I threw rocks back to the baboons. I set foot in Joppa.
My father would never know. I became a ghost when I left–something transient that never returns.
Un petit rappel régulier que j'aime faire, et une exceptionnelle ressource pédagogique : Si vous souhaitez en apprendre plus sur les fondations théoriques du développement de logiciels (ou l'enseigner), apprendre l'assistant de preuve #Coq au passage (ou l'enseigner), je vous conseille de jeter un oeil au magnifique #SoftwareFoundations de Benjamin Pierce et al. https://softwarefoundations.cis.upenn.edu/ Il contient aussi un plan conseillé pour enseigner sur un semestre, un par chapitre. Foncez !
I have no problem with #Coq changing its name except I dont think its going to work, Coq has been around too long and there's too many decades of pre-existing material created in that name for people to shift gears, explaining the name change to non-users will become exhausting.
If they simply changed the pronunciation to the natural anglophonic "coke", it would be fine, but "Rocq?"
We are organizing the FP Dag aka Dutch Functional Programming Day on Friday the 5th of January in Delft. People from neighboring countries are also very welcome to join!
The (soft) registration deadline is on the 22th of December (next Friday), so get your tickets soon!
Tomorrow is already the deadline for the third edition of #WITS, the Workshop on the Implementation of Type Systems, colocated with #POPL 2024 in London. The page limit is one page, but just a single-paragraph abstract with an interesting idea for a talk is also very welcome! In particular contributors to #Haskell#OCaml#Rust#Scala#Coq#Lean#Agda#Idris#Cedille#Arend#CoolTT and even #TypeScript are warmly invited to give a talk about their experiences with implementing type systems.
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
As a Freudian and a Platonist (which is actually, per Plato, an affirmation of the generic, anomalous, supersuccessive and subjective nature of truths) I can't help but recognize the #constructivist wager in #mathematics as an appearance of what psychoanalysts call "the university discourse", the discourse concerned with the management of truths rather than their promulgation. At the same time, as a hacker, I cant help but be interested in #HoTT, and recognize that what is happening there is beautiful and even novel (for hackers, at least). And as a Benjaminian, which is to say a dialectical messianist, I cant help but think that our epoch's imperative to reduce all phenomena to computation is what he called "the aestheticization of politics", nor do I doubt that what our moment requires is the "politicization of art", if we wish to avoid the worst of all possible worlds.
Hackers often fancy themselves as misunderstood mathematicians, but any serious inquiry into the work of hacking reveals that the hacker is an artist whose medium is rithm or caesura, and that hacking is thus in truth a form of poetics; albeit the poetics of mechanics*. On the other hand, mathematicians often fancy themselves as misunderstood poets, even if they can't be bothered to study in detail the playful successions of caesura that differentiate rithm for the poet, preferring to deal with mathematical concepts like topoi and posets. On the other hand, some mathematicians are also poets, and may be drawn to #Coq et al, and may even use it to produce novel results in mathematics. But I dont think that will be a matter of of the superiority of a constructivist research program, just as producing an immortal program such as emacs doesn't imply the eternality of "GNU slash Linux". Its rather because being a mathematician doesn't preclude one from being a hacker, and most hackers are likely to become fascinated by ITPing if they give it a try. But to demand that all mathematicians subordinate their curiosity to that of the hacker-mathematician is absurd, and furthermore, ethically obscure.
The point of this post being that I contain multiplicities, and so do you.
I just finished the first chapter of @d_christiansen's Functional Programming in #Lean, and I gotta say, theorem provers consistently win when it comes to pure fun. And Lean has been incredibly easy to dive into, find out where things are, and start... programming with, it really just feels like (or rather, is) another functional programming language, but with all the fanciness of dependent types.
I think #Agda is by far the nicest purely at the language level (I'd probably consider Agda the prettiest language after Scheme), but 2gb is a lot of space, especially for someone like me that has lots of large 3D scene files, with massive textures, and am constantly making space on my laptop. #Coq is smaller then Lean, but a lot of OCaml also bleeds through, which is a great language, but not the most elegant, and I'm just trying to grill.
#Idris is really great and the one I've spent the most time with; I was even split between diving deep into either Idris or #Scheme a few years ago and chose the latter, as Edwin Brady's book is one of the best general introductions to FP I have read. But what I'm ultimately interested in exploring is Lean's hygienic macro system, and I'm overall really digging the lispyness hiding within Lean's mixfix notation
i'm trying to understand how far one can get writing explicit proof objects in #coq. nothing i can find immediately (e.g. https://www.seas.upenn.edu/~cis5000/cis500-f14/sf/ProofObjects.html) shows syntax for inductive proofs? i tried writing one with a recursive call and got a "reference not found", so i'm guessing it shows up as an argument to the inductive case or something?
"The focus of my research is applying #fp, in particular #chez#scheme, to low-level problems — the type of situations that usually call for #rust or #c"
— highly recommended talk on programming with serialized data from @vollmerm @ #ELSconf
> "are there any texts on typing scheme you'd recommend?"
For calculus of constructs, I recommend Benjamine C. Pierce "Software Foundations," which you can read online. It uses #Coq for the exercises, and you can use the "Proof General" front-end to Coq in #Emacs to do the exercises on your own computer. I've only got through the first chapter of the first volume so far though: https://softwarefoundations.cis.upenn.edu/
I don't have any one that kind of summarizes or compares all type systems. I ran across all these different type systems at times throughout my life. CSP and Pi Calculus I was introduced to in a class in graduate school, the original textbook on CSP by Tony Hoare was pretty good, pretty easy to read. Hindley Milner I just learned by using Haskell. Separation logic is described in this paper, but pretty heavy on mathematics: https://www.cs.cmu.edu/~jcr/copenhagen08.pdf