Mastodawn

The #idris2 tutorial book requires #rakulang 🦋 in the build process!

https://github.com/idris-community/idris2-tutorial?tab=readme-ov-file#raku-dependencies

This is the program: https://github.com/idris-community/idris2-tutorial/blob/main/scripts/build-book

The code:
1. Is well commented and readable.
2. Uses Raku's parallelism features.
3. Uses Raku's next-gen regexes.
4. Runs command line programs, collects the output.

Cool stuff! 😎

What's your favourite unexpected/serendipitous usage of Raku in the wild?

GitHub - idris-community/idris2-tutorial: A comprehensive tutorial for the Idris2 programming language

A comprehensive tutorial for the Idris2 programming language - idris-community/idris2-tutorial

GitHub

Show thread

Stefano Volpe

Oct 4

@spacefinner considering getting back to #Idris2 for my first #AdventOfCode. I mostly use #Agda nowadays

José A. Alonso Sep 20, 2025

Readings shared September 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/20-readings_shared_09-19-25 #Agda #CoqProver #ITP #Idris2 #LeanProver #Rocq

Readings shared September 19, 2025

The readings shared in Bluesky on 19 September 2025 are: Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. #ITP #LeanProver The mechanization of science ill

Vestigium

José A. Alonso Sep 19, 2025

Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. https://arxiv.org/abs/2509.15015 #ITP #CoqProver #Idris2

Theorem Provers: One Size Fits All?

Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their usability, alongside the problem domain in which they are employed. We test-drive two such provers, Coq and Idris2, by proving the correctness of insertion sort, before providing a qualitative evaluation of their performance. We then compare their community and library support. This work helps users to make an informed choice of system, and highlight approaches in other systems that developers might find useful.

arXiv.org

Ben Clifford Aug 30, 2025

Did this manic 20 slide lightning talk reimplementing part of @ParslProject using #Rust #Idris2 #Elixir

https://parsl-project.org/parslfest/2025/benc-3lang-interchange.pdf

Ben Clifford Aug 26, 2025

valgrinding the #idris2 ffi again when i should really be making slides

Jan de Muijnck-Hughes Aug 20, 2025

Double-checking the lab software for next academic year:

Dafny was installed correctly! However, installing the VSCode app also installs the latest version.... Getting Dafny working in Emacs was okay. But I know what I am doing.

Idris2 was installed correctly! Getting Emacs to work was not a pain, but I know what I am doing... Getting VSCode to work however, is different. I do not want students to install things unnecessarily...

I usually let students fend for themselves.

This year I think I will provide a minimal emacs config and be explicit about expectations....

I wish I could chat to others who teach #idris2 I fear it is only myself....

#idris2 felt less polished|stable than #idris 1 .
& with non-unix builds.
& with IDE support.

Idris2 forced me to compile, install, learn nvim (neovim), to just get IDE features that were available 10 years ago in idris1 VSCode plugin.

Ben Clifford Aug 20, 2025

i was actually hoping to get #idris2 C backend working because I thought i might get nicer valgrind stack traces out than out of the scheme backend.

I fixed up holes (which wouldn't compile) and now I get FFI missing headers for my own libraries.

So back to the scheme version. which doesn't run properly in this debian inside valgrind unless I set some path, which might be a scheme bug from years ago not yet propagated.

teenage fun.

lxsameer Jul 25, 2025

I owe a lot to a few programming languages that taught me how to design a language, both from an engineering standpoint and computer science.

#Lisp & #haskell for what a good programming language might look like.

#Agda, #Idris2, #lean4 to show me how useful dependent types are.

#C++, to teach me what to avoid

#python, #javascript to be such giant examples of shitty languages and give me hope that I can do better. 😂