check if a #regex is valid but in #idris
https://www.reddit.com/r/ProgrammingLanguages/comments/hb6rn4/dependent_types_and_usability/

L' #IDRIS, centre de calcul du #CNRS héberge une émission sur les progrès de l' #IA (pas seulement générative) appelée Panoram'IA. Le prochain numéro sera enregistré en direct de l'IDRIS et reviendra entre autre sur le pretraining de #lucie: https://www.youtube.com/@idriscnrs

Ça sera le vendredi 28 février à 10h00.

Seront aussi discutés l' #ia Summit de #Saclay et l'actualité de la recherche en IA, bien évidemment.

Malheureusement je ne pourrai pas probablement pas en être, mais si il y en a que cela intéresse ici...

Who da thought! Having multiple distinct uses of `(=)` in your language would be confusing...

For assignment, as a type, and for equations...

Might start not using `(=)` as the type for equality, and use `(===)` more...

Perhaps, for next generation of #Idris , it would be good to have a proper user study on what is appropriate syntax for key aspects of the language.

The strangeness budget for imperative programmers in #CS886 has been blown! The students are warming to #Dafny more! (Rapid introductions aside) The reaction towards the two languages was expected. They do not have a functional, nor PLT background.

I should talk to colleagues about their experience in the other course....

I have a funded #PhD position for UK students, available with myself and @bentnib

This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.

Deadline: Thursday 20th March 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

For now more details about the project are on my personal website.

https://tyde.systems/page/position/2025-jarss/

Please spread the words.

Benchmarking native multicore #Idris on a 64-core machine sure is fun

#Idris is such an underrated programming language…

Chapter 8 of Type Driven Development with #Idris is really tough and fascinating.

Sean Haas of @adventofcomputing has a fascinating episode out about #IDRIS, a reimplementation of #UNIX for a variety of early personal computers with #Intel8086, #Motorola68000 CPUs as well as #DEC #PDP11. Bizarrely, the OS seems mostly lost.

adventofcomputing: Episode 149 - IDRIS is Not UNIX

https://www.patreon.com/posts/episode-149-is-119316624

https://en.m.wikipedia.org/wiki/Idris_(operating_system)

A version of IDRIS that starts from #DOS is available on GitHub, though!

https://github.com/hansake/Whitesmiths-Idris-OS/tree/main/co-idris_setup

“Type Driven Development with Idris”book states that in #Idris interfaces can have any number of parameters, even zero.
I struggle to imagine a case where having zero parameters can be useful. Any idea?

I think I owe @edwinb an apology. I was deeply sceptical about the utility of his funky types in #Idris a few years ago, but having now listened to the interview he did with the #CoRecursive podcast, and also after exposure to #Rust's magnificent error messages, I'm now convinced. https://corecursive.com/006-type-driven-development-and-idris-with-edwin-brady/

It’s easy to prove that Boolean negation is an involution, but can you have “definitional” involution in a dependently typed language like #Idris ?
It kind of works if you use the Church encoding of Booleans, but then you can’t pattern match on those.

Current status: reading chapter 6 of Type Driven Development with #Idris.

It is wonderful. Pure joy.

I’m reading parallel “Type-Driven Development with #Idris” and “Patterns, Principles and Practices of #DDD”.

The difference is paramount: as serious and rigorous as one is, so vague, unnecessarily verbose, and tree-hugging the other is.

So far, #Idris looks beautiful: like a simpler and way more expressive #Haskell.

Current status: just started reading “Type-Driven Development with #Idris”

#Dafny sadly doesn't have support for #literate_programming a cool feature I think they should support!

Whilst I do not think libraries nor programs should be coded in the literate style, informal presentations and lectures and notes should be!

For #Idris, I have often wrote the presentation in OrgMode and used polymode to mix orgmode and idris-mode together.

Org-mode provides more precision on revealing items and storing reading notes. (one step away from writing that book as well...)

Idris' own mode enables interactive editing.

Key for polymode to work is that the compiler must be literate enabled.

does #Idris (#Idris2) have a named record constructor syntax? like this?

```
example = Person{ name = "John Doe", admin = True }
```

I just completed "Garden Groups" - Day 12 - Advent of Code 2024 #AdventOfCode https://adventofcode.com/2024/day/12

203 lines of #Idris pushed.

I just completed "Plutonian Pebbles" - Day 11 - Advent of Code 2024 #AdventOfCode https://adventofcode.com/2024/day/11

83 lines of #Idris pushed to my repo.

I think I'm going to further refine this. It's still slower than I'd like.