Interested in a PhD studentship in the Functional Programming Lab in Nottingham? Fully-funded studentships are currently being advertised; deadline 6 January 2027. Please share, and encourage excellent students to apply!  https://people.cs.nott.ac.uk/pszgmh/phd-advert.html

It's a 21 minute video. The first 9 minutes are demos and walkthrough. The technical explanations and my thoughts start at 9:56.

One of my friends introduced to me this Agda tutorial: Let's Play Agda, and I enjoyed it. However, its implementation relies on a backend running instances of Emacs, which, is obviously not friendly to mobile users. Therefore, I forked the repo, replaced the backend with a WASM version of VS Code and Agda, and made the UI more modern (TBH, that means more LLM-ish). Now I can easily play Agda on my phone!

My own version of Let's Play Agda is here:

https://andyshiue.github.io/lets-play-agda/

Even though I know I have the right to publish the adapted version because the original Agda files are licensed by CC BY-SA, I've contacted the original author, iblech, to seek for his opinions. However, he hasn't replied yet and it's been several day so I decided to directly post it here.

Hey everyone!

With all the attention formal verification has been getting lately, particularly at the intersection of AI, theorem proving, and programming languages, we decided to put together FVjobs, a community-maintained job board to help people figure out who's actually hiring.

https://github.com/typetheoryforall/FVjobs

The board covers formal verification, proof engineering, automated reasoning, verified compilers, and AI-assisted theorem proving, among other related areas.

We're also keeping track of which tools companies use (Lean, Rocq, Isabelle, SMT, etc.), remote work options, and geographical restrictions. Hopefully, this makes it easier to find relevant opportunities without digging through dozens of company websites.

For now, we're keeping things simple with GitHub and GitHub Issues. Depending on how the project develops and whether there's enough community interest, we might eventually build a dedicated website.

This is a community effort, and we'd love your help keeping it up to date!

If you know of an open position, no GitHub knowledge is necessary. You can simply fill out this form:

https://github.com/typetheoryforall/FVjobs/issues/new?template=new-job.yml

Of course, issues and PRs are also very welcome.

Feedback and suggestions are appreciated, especially regarding what would make this resource more useful to the community!

In this episode, Davide and Giacomo share: 
- How AtomVM squeezes the BEAM onto memory-constrained devices 
- Why Gleam and AtomVM are a perfect match for hobbyists and students 
- Davide's "scar story" of a buggy AtomVM-powered home thermostat leaving him debugging in the cold 
- The trade-offs of the AtomVM standard library and how to extend it 
- Writing Gleam bindings for AtomVM features via Erlang FFI 
- Example projects to tackle as an embedded Gleam beginner 
- What's possible with $2 boards, some sensors, and MQTT 

https://youtu.be/57Vhx7FHk34

Hello everyone! I'm taking a functional programming course in python and was wondering if there were any valuable resources (preferably youtube channels) that cover things like LLists, higher order functions, efficiency, data structures, searching, sorting, etc.

Any help would be appreciated thanks :)

Hello,
Not sure how useful JavaScript/TypeScript are in the FP community.
If they are, I've just made yet another take on enforcing immutability in JS/TS - via a fast linter.
Essentially, it bans let/var, reassignments, non-readonly object and class properties.
To use any of the above, an explicit linter disable comment is needed.
So far, 3 variants of disable comments are available - `// ptsl-disable-fn` (function body scoped), and more classic `// ptsl-disable-line` and `// ptsl-disable-next-line`

So, the following code will be banned by linter:

const nextNum = () => {
  let x = 0; // Do not use let/var - only use const
  const increment = () => {
    return x += 1; // Do not reassign variable's value unless absolutely necessary.
  }
  return increment;
};

A `// ptsl-disable-fn` comment will make it pass:

const nextNum = () => {
  // ptsl-disable-fn
  let x = 0;
  const increment = () => {
    return x += 1;
  }
  return increment;
};

Any feedback welcome.