nomeata

markuswerle, 1 month ago to random German

Wie geil ist das denn? Der Chaos Computer Club Essen hat das Grundgesetz nicht nur bei GitHub hochgeladen, sondern so aufbereitet, dass alle Änderungen durch Git Commits dargestellt sind und die Git Kommentare alle wesentlichen Infos enthalten.

Und natürlich haben die Bundespräsidenten mit korrektem Datum committed!

https://github.com/c3e/grundgesetz/commit/c4646b072899a4c1acd3e892770bb2fc78fd40b7

haskell_foundation, 1 month ago to haskell

The term 'telemetry' can raise a lot of concerns, especially within the realm of #OSS. In the latest episode of #TheHaskellInterlude, Joachim Breitner and Andres Löh interview @avi_press, the CEO of @scarf_oss. Learn more about the episode here: https://haskell.foundation/podcast/47/
#Haskell

Moorknipser, 1 month ago to photography German

Sowas mag ich!
#fotografie #photography

BahnAnsagen, 2 months ago to random German

++ BAHN-ANSAGE DES MONATS, 03/2024 ++

Jose_A_Alonso, 2 months ago to haskell

Abstracting denotational interpreters. ~ Sebastian Graf, Simon Peyton Jones, Sven Keidel. https://arxiv.org/abs/2403.02778 #Haskell #FunctionalProgramming

mangoiv, 3 months ago to haskell German

GHC2024 has landed on HEAD and will be part of GHC 9.10, notable changes include:

• GADTs + MonoLocalBinds
• DataKinds
• LambdaCase

Sadly no BlockArguments (Haskeller appear to love their dollars) and TypeData (time hasn’t come I guess)

Also thank god no ImpredicativeTypes and TypeFamilies

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12084

Also please thank @nomeata for pushing this forward! 👏

#haskell

leanprover, 3 months ago to random

Lean 4.6.0 has been released

https://lean-lang.org/blog/2024-2-29-lean-460/

sgraf, 3 months ago to random German

How do people (well, semanticists) say in short terms that some syntactic restriction is necessary to "work around the lack of full abstraction" in their semantic domain?

E.g., I have some lemma f(d) <= g(f,d) that I need to prove correct, and I can only do so if I assume that f = [[λx.e]] for some e. I say "this syntactic restriction is necessary due to a lack of full abstraction", which seems very indirect.
Is there a more succinct term to describe this?

https://www.pls-lab.org/en/Full_abstraction

mangoiv, 3 months ago to haskell German

https://haskell.foundation/podcast/43/

Super interesting podcast episode. Ivan Perez is interviewed by @wouter and @kosmikus. He’s a researcher at NASA who develops the copilot embedded domain specific language for monitoring state transitions of the software running on their devices.

#haskell

stefan, 4 months ago (edited 4 months ago) to til

So apparently the term "patch" in software development comes from punched paper tape.

"Small corrections to the programmed sequence could be done by patching over portions of the paper tape and re-punching the holes in that section."

https://chsi.harvard.edu/harvard-ibm-mark-1-language

#til #computers #development #language #history

bobkonf, 4 months ago to random

12 hours left to get your Early Bird Ticket to #BOBkonf2024!

Find out more and get your tickets here:
https://bobkonf.de/2024/registration.html

peterb, 5 months ago to random

New Video: QED, the Propositional Logic Game https://youtu.be/yJ_ZIWhHffQ

Hat tip / blame to @aris_uu on Twitter for letting me know this exists and thus inadvertently forcing me to make the video, and a hat tip to @nomeata for getting me interested in the problem space in the first place. Apologies to @tao for the many, many things I probably got wrong when describing the project.

mangoiv, 6 months ago to haskell

The glorious Glasgow Haskell Compiler is preparing for the next GHCxxxx edition. These are bundles of extensions that are considered popular, stable and useful and should be offered to any Haskeller out there. There was already one such edition, GHC2021, replacing the original Haskell standards process after GHC had become basically the only widely used Haskell implementation.

If you want to be part of this proposal, this is your chance, vote now and make Haskell more convenient for yourself!

Big thanks to @nomeata for driving the process.

#haskell

https://discourse.haskell.org/t/ghc2024-community-input/8168

boilingsteam, 7 months ago to linux

NixOS Reproducible Builds: minimal ISO successfully independently rebuilt: https://discourse.nixos.org/t/nixos-reproducible-builds-minimal-installation-iso-successfully-independently-rebuilt/34756 #linux #update #foss #nixos #distro #reproducible #build #milestone

tao, 7 months ago to random

As a consequence of my #Lean4 formalization project I have found a small (but non-trivial) bug in my paper! While in the course of formalizing the arguments in page 6 of https://arxiv.org/pdf/2310.05328.pdf , I discovered that the expression ( \frac{1}{2} \log \frac{n-1}{n-k-1} ) that appears in those arguments actually diverges in the case ( n=3, k=2)! Fortunately this is an issue that is only present for small values of (n), for which one can argue directly (with a worse constant), so I can fix the argument by changing some of the numerical constants on this page (the arguments here still work fine for ( n \geq 8), and the small (n) case can be handled by cruder methods).

Enclosed is the specific point where the formalization failed; Lean asked me to establish ( 0 < n - 3 ), but the hypothesis I had was only that ( n > 2 ), and so the "linarith" tactic could not obtain a contradiction from the negation of ( 0 < n-3).

I'll add a footnote in the new version to the effect that the argument in the previous version of the paper was slightly incorrect, as was discovered after trying to formalize it in Lean.

barubary, 8 months ago to haskell

Today I spent a few hours trying to track down a problem deep in a helper module of a complex production application written in #Haskell. Among other things, it involves threads, a monad transformer stack (3 or 4 levels deep, I think?), an SQL database, and HTTP calls to an external service.

In the end, I managed to boil one issue in the code down to the following crucial lines:

forever_mpl :: Monad m => m a -> m b<br></br>forever_mpl m = fix (m >>)<br></br><br></br>forever_mpf :: Monad m => m a -> m b<br></br>forever_mpf m = fix (self -> m >> self)<br></br>

In theory, both of these should be equivalent to forever from the base library. However ...

In one place in the code, using forever_mpl (the first definition) works correctly: It repeats an action forever. But switching to forever_mpf (the second definition) makes the code hang instead (at 0% CPU). Why?!

I know the answer now, so here's a #debugging challenge: Can you think of a reason why these two definitions should behave differently? Can you implement a Monad instance with a >> that distinguishes between them somehow?

maralorn, 8 months ago to random

@nomeata The phrase "Let the bikeshedding begin" made my day, thx.

https://github.com/ghc-proposals/ghc-proposals/pull/569

rml, 8 months ago to rust

#GCC size: 343Mb*
#Rust size: 1Gb
#GHC size: 1.4Gb
#Clang size: 1.7Gb

#Chez #Scheme size: 5mb

[ * ] all based on the results of using #guix size, removing common and documentation-based dependencies such as ncurses, bash, and zlib

nomeata, 8 months ago to haskell

At my talk at #ICFP2023 I claimed that with observable sharing one can write a parser combinator library where left-recursion works (in the presence of sharing), and someone asked if I had, and I had to admit I hadn’t, so the next day I did:
https://www.joachim-breitner.de/blog/807-Left_recursive_parser_combinators_via_sharing
#Haskell

leanprover, 9 months ago to random

We're pleased to announce the first official release of Lean 4!
Release notes: https://github.com/leanprover/lean4/releases/tag/v4.0.0
Post on the community blog about future release cycles: https://leanprover-community.github.io/blog/posts/first-lean-release/

funarch, 9 months ago to random

If you‘re at #icfp on Friday, don‘t miss the first ACM Workshop on Functional Software Architecture! https://www.functional-architecture.org/events/funarch-2023/

jreusch, 9 months ago to NixOS

One of my favorite things about #NixOS is that I can just add my own patch to a package with like 3 lines of code and it just works

I had to modify the command line args that NetworkManager passes to openfortivpn

Now I got to figure out how to talk to people to maybe get this added to nixpkgs, wish me luck

bobkonf, 10 months ago to random

Revisit @nomeata's #BOBkonf2023 talk "Getting recursive definitions off their bottoms" here: https://bobkonf.de/2023/breitner.html

nixos_org, 10 months ago to random

🚀 NixCon 2023 is looking for sponsors 🚀

NixCon brings together developers, contributors, enthusiasts, and organizations from all corners of the world to learn, share knowledge, and foster innovation in the Nix ecosystem.

Sponsorship tracks ➡️ https://discourse.nixos.org/t/nixcon-2023-sponsorship-tracks/29550

johncarlosbaez, 11 months ago (edited 8 months ago) to random

It's time for me to reread Lockhart's lament:

"All this fussing and primping about which “topics” should be taught in what order, or the use of this notation instead of that notation, or which make and model of calculator to use, for god’s sake — it’s like rearranging the deck chairs on the Titanic! Mathematics is the music of reason. To do mathematics is to engage in an act of discovery and conjecture, intuition and inspiration; to be in a state of confusion — not because it makes no sense to you, but because you gave it sense and you still don’t understand what your creation is up to; to have a breakthrough idea; to be frustrated as an artist; to be awed and overwhelmed by an almost painful beauty; to be alive, damn it. Remove this from mathematics and you can have all the conferences you like; it won’t matter. Operate all you want, doctors: your patient is already dead."

The whole thing is here:

https://www.mimuw.edu.pl/~pawelst/rzut_oka/Zajecia_dla_MISH_2011-12/Lektury_files/LockhartsLament.pdf