@jesper@agda.club
@jesper@agda.club avatar

jesper

@jesper@agda.club

Once Jesper Cockx but now running Agda instead. Assistant professor @DelftPL.

Talk to me about:

  • Dependently typed programming
  • Tabletop role-playing games
  • Playing bassoon and clarinet
  • Effective altruism
  • Climate change
  • Neurodiversity
  • Mindfulness
  • Creativity
  • Hiking and landscape photography

This profile is from a federated server and may be incomplete. Browse more on the original instance.

jesper, to Blog
@jesper@agda.club avatar

I wrote a blog post about Agda Core! It's a bit long and not very polished, but I'm happy to have it finished (thanks to a long and distraction-free train ride to Swansea).

jesper.cx/posts/agda-core.html

mangoiv, (edited ) to random
@mangoiv@functional.cafe avatar

Who’s coming to ZuriHac?! I’m so excited!

#haskell

jesper,
@jesper@agda.club avatar

@mangoiv
Where is the "I'm giving an Agda tutorial at ZuriHac" option?

jesper, to random
@jesper@agda.club avatar

Reminder that the deadline for TyDe is in less than one month! We accept both full papers (with a formal proceedings) and extended abstracts with all your crazy ideas.

icfp24.sigplan.org/home/tyde-2024#Call-for-Papers

jesper, to haskell
@jesper@agda.club avatar

This is a great blog post on the WellTyped blog on specialization in Haskell! It's a good reminder that I (or someone) should really get around to getting rid of -fexpose-all-unfoldings and -fspecialize-agressively in the Agda codebase.

well-typed.com/blog/2024/04/choreographing-specialization-pt1/

(Also I didn't know about -flate-specialise and -fpolymorphic-specialisation, though I think I'd rather avoid relying on even more flags.)

jesper, to random
@jesper@agda.club avatar

How does an astronomer trust the results of their telescope? How does a physicist trust the results of their spectrometer? How does the engineer trust that the bridge they built won't collapse?

Proof assistants are our telescopes, our spectrometers, our bridges. We should do our very best to build them as well as we can, but ever getting to 100% certainty is an illusion.

jesper, to random
@jesper@agda.club avatar

Is there anything known about the efficiency implications of using HOAS for representing the (internal) syntax of a lambda calculus instead of de Bruijn syntax? Assuming one can get away with it, it seems like it could theoretically speed things up compared to looking up things in lists. OTOH functions can do arbitrary things, so I imagine much would depend on how you actually construct these.

Maybe @AndrasKovacs has an idea?

jesper,
@jesper@agda.club avatar

@wouter That's really interesting, thanks! My intuition is that (1) doing substitution is really bad for efficiency and (2) the efficiency of HOAS compared to an environment machine will depend greatly on how the HOAS was constructed in the first place. I'll have to study Stephanie's results in more detail to see if they match this intuition..

jesper, to random
@jesper@agda.club avatar

New blog post about core languages and : "6 Reasons in favor of a core language, and 5 against"

jesper.cx/posts/why-not-a-core-language.html

jesper, to random
@jesper@agda.club avatar

Ok so let me get this straight:

  • tries to install linux mint alongside windows 11 on my new laptop
  • cannot get to boot menu because of windows fast boot
  • goes through the 7 levels of nested config menus to disable fast boot
  • cannot boot from usb stick because secure boot is enabled
  • disables secure boot and starts installation
  • cannot resize windows partition because it has BitLocker
  • tries to boot into windows again to disable bitlocker
  • cannot boot into windows because secure boot is disabled

Ok I get it, you don't want me to use Windows, you didn't have to be so rude about it.

jesper, to FunctionalProgramming
@jesper@agda.club avatar

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!

https://www.tudelft.nl/fpday-2024

avandeursen, to random
@avandeursen@mastodon.acm.org avatar

Very interesting long read on “value capture” — when measurements like grades, citation counts, or step counts take over the true values (learning, writing, health) you actually care about. Also related to “stop the numbers game” by David Parnas (“Counting papers slows the rate of scientific progress”).

https://philarchive.org/rec/NGUVCH
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=a185c913482fc0d0e42291bec4748e24438c130b

Via @smallcircles, @aredridel
#ErkennenWaarderen #RecognitionRewards

jesper,
@jesper@agda.club avatar

@avandeursen

From the abstract this sounds a lot like Goodhart's Law: "When a measure becomes a target, it ceases to be a good measure." Or is there more to it than that?

jesper, to random
@jesper@agda.club avatar

OH FUCK FUCK SHIT WHY DO PEOPLE VOTE FOR THIS STUPID RACIST ASSHOLE

jesper,
@jesper@agda.club avatar

@anuytstt

Meanwhile I've been listening to the audiobook of The Lost Cause by @pluralistic and it's very cathartic to imagine a world in the not-so-distant future where these people are relegated to the past like the fossils they are.

jesper, to haskell
@jesper@agda.club avatar

I really need this in my Haskell: github.com/ghc-proposals/ghc-proposals/pull/621

Sadly, even if it gets merged it will take at least 5 more years before we can use it in the Agda codebase.

philipdutre, to random Dutch
@philipdutre@mastodon.online avatar

Als je er over nadenkt is het knettergek dat een voorzitter van een nationale politieke partij een 30- of zelfs 20-jarige is. Zeker in ons particratisch systeem waarbij er zeer veel macht bij de voorzitter ligt kan je dat eigenlijk toch niet verantwoorden?

jesper,
@jesper@agda.club avatar

@philipdutre
Waarom niet? Als ik om me heen kijk zie ik weinig bewijs dat oudere mensen per definitie meer voeling hebben met de realiteit of betere beslissingen nemen.

theautisticcoach, to actuallyautistic

It’s Monday comrades.

What are your biggest challenges?

@actuallyautistic

jesper,
@jesper@agda.club avatar

@theautisticcoach
@actuallyautistic

Prioritizing.
Noticing when I'm overwhelmed.
Being kind to myself.

theautisticcoach, to actuallyautistic

Do my comrades love their plushies / stuffed animals?

Are they a big part of your life?

What do they mean to YOU?

Who are your favorites? Where are they from? Is there a story?

Introduce them!

@actuallyautistic

jesper,
@jesper@agda.club avatar

@theautisticcoach
@actuallyautistic
Ooh time for a group picture! The guy in the middle has been with me for as long as I can remember. The cat's the most recent addition, it's Mae from Night in the Woods. And the big & little cow... well what can I say, cows are just cute? The hat's a souvenir from Skye from our family trip to Scotland.

jesper, to haskell
@jesper@agda.club avatar

Tomorrow is already the deadline for the third edition of , the Workshop on the Implementation of Type Systems, colocated with 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 and even are warmly invited to give a talk about their experiences with implementing type systems.

Call for papers: popl24.sigplan.org/home/wits-2024#Call-for-Participation
Submission link: wits24.hotcrp.com/

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • JUstTest
  • kavyap
  • DreamBathrooms
  • thenastyranch
  • magazineikmin
  • tacticalgear
  • cubers
  • Youngstown
  • mdbf
  • slotface
  • rosin
  • osvaldo12
  • ngwrru68w68
  • GTA5RPClips
  • provamag3
  • InstantRegret
  • everett
  • Durango
  • cisconetworking
  • khanakhh
  • ethstaker
  • tester
  • anitta
  • Leos
  • normalnudes
  • modclub
  • megavids
  • lostlight
  • All magazines
    •