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.

Hi all, I've just released a new property-based testing library for Java. It's called Presume, and it's a direct-style interpretation loosely based off of Python's Hypothesis, rather than the more common QuickCheck or Hedgehog based options currently available.

If you're new to property-based testing I have an explanation of the paradigm in the docs.

Why I think this may be interesting to this subreddit: Aside from PBT and functional programming going hand-in-hand, the implementation was also a fun journey through functional-style Java. I ended up implementing maybes, rose trees, immutable lists, multiple kinds of zippers and a range of ADTs using Java's records and pattern matching. I'm relatively new to Java (after using TypeScript for years) and am sinking into the uncomfortable realization that Java is actually pretty nice for FP. I definitely could not have implemented this without records and patterns. I believe the core shrinking algorithm is novel; it's similar to Hypothesis's, but it allows for more control over generation size and intentional edge case generation, and follows simpler heuristics (albeit with a potentially more troublesome implementation) than what is described in the main Hypothesis paper. I plan on blogging about the algorithms in the future but I'm also happy to answer questions about them here.

Why you might want to use this, rather than some of the possible alternatives:

• It's not vibecoded. I used a nonzero amount of AI (see below) but the core architecture, algorithms, and API design are all fully human. It's undergone a significant amount of iteration and hand polishing until it's felt properly ergonomic

• It's released under a clean MIT license, with no unusual exceptions

• It provides an imperative API for working with test generators, which IMO can make it significantly easier to generate complex and recursive data. No special lazy combinators or deep function nesting are needed to define recursive ASTs, for example. Functional approaches are still supported.

Why you might not want to use this:

• I used a nonzero amount of AI (which is why I'm not also posting this in r/Java). Specifically, some of the Gradle configuration came from an LLM, and I used an agent to fix and test the bit twiddling implementation in the long, float, and double generators. Being new to Java I also frequently consulted AI summaries while searching for ways of doing things. If you want something completely AI-free then jqwik is a better fit for you.

• This is a very new project; I've been working on it for 3 months but I still haven't implemented a lot of convenience combinators or even thought about what state machine testing should look like here. There are still some TODOs here and there, and I haven't made certain spots stack-safe yet so generators can currently only produce trees that are a few thousand levels deep at most.

• The fact that the shrinking algorithm is novel means that it may have limitations that I'm not yet aware of. I'm hoping to try to do a side-by-side comparison with Hypothesis at some point to see whether there's any breakdowns.

• There's not many docs and no docstrings. I plan on fixing this soon, but I wanted to release this into the world before a specific event next week, and this is as far as I've gotten thus far.

• Currently Java 25 only; I'm probably going to go back and make it Java 21 compatible in the near future. I don't think it'll go back any further than that though because this would not be remotely maintainable without records/pattern matching.

Happy to answer questions, and I'm hoping that this will be helpful for someone! I'm also interested in feedback on the implementation from anyone with more Java skills than myself, because I'm very much still learning the language.