LHolten @LHolten@qoto.org

Me having to touch #Python and #Ruby again at work today after a blissful week of working on #Rust PRs 🙃

#programming #coding #jokes

#LedByDonkeys zet de wandaden van Musk eens even goed op een rijtje en in het zonnetje.

as far as im concerned really theres only two types of software: database, or compiler. your task is to work out which one of the two your idea fits into

New paper by @liesnikov and yours truly at APLAS 2024: "Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language", in which we demonstrate how to use well-scoped syntax, indexed datatypes, and erasure annotations to develop a certified type checker for a small subset of Agda.

link.springer.com/chapter/10.1007/978-981-97-8943-6_4

PDF: jesper.cx/files/building-a-cbc-type-checker.pdf

#Agda #DependentTypes #FunctionalProgramming

RustNL is proud to announce we will host the first "Rust All Hands" since 2018!
The All Hands is organized in close collaboration with the @rust project and with support of the Rust Foundation.

The "Rust All Hands" event is where all members of the Rust project come together in person to collaborate on the future of Rust. 🎉

The All Hands will be part of RustWeek 2025, in Utrecht, NL in May 2025.

https://blog.rust-lang.org/inside-rust/2024/09/02/all-hands.html

Public transport should be free.

This post is brought to you by the announced 8.7% increase of train ticket prices in the Netherlands.

The Agda Team is pleased to announce a release candidate for Agda 2.7.0.

Highlights

Mimer, a re-implementation of the “auto” term synthesizer, replaces Agsy.
New syntax using x ← e to bind values on the left-hand-side of a function clause.
Instance search is more performant thanks to a new indexing structure. Additionally, users can now control how instances should be selected in the case multiple candidates exist.
User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections are now on by default.

GHC supported versions

Agda 2.7.0 RC 1 has been tested with GHC 9.10.1, GHC 9.8.2, GHC 9.6.6, 9.4.8, 9.2.8, 9.0.2, 8.10.7, 8.8.4 and 8.6.5 on Linux, macOS and Windows.

Installation

Agda 2.7.0 RC 1 can be installed using cabal-install or stack:

Getting the release candidate

$ cabal get

https://hackage.haskell.org/package/Agda-2.6.20240714/candidate/Agda-2.6.20240714.tar.gz

$ cd Agda-2.6.20240714

a. Using cabal-install

$ cabal install -f +optimise-heavily -f +enable-cluster-counting

b. Using stack

$ stack --stack-yaml stack-a.b.c.yaml install --flag

Agda:optimise-heavily –flag Agda:enable-cluster-counting

replacing a.b.c with your version of GHC (8.8.4 or higher).

The flags mean:

optimise-heavily: Turn on extra optimisation for a faster Agda. Takes large resources during compilation of Agda.
enable-cluster-counting: Enable unicode clusters for alignment in the LaTeX backend. Requires the ICU lib to be installed and known to pkg-config.

These flags can be dropped from the install if causing trouble.

Standard library

You can use the experimental branch of the standard library with Agda 2.7.0. This branch is available at

https://github.com/agda/agda-stdlib/

Changes and fixed issues over Agda 2.6.4.3

https://hackage.haskell.org/package/Agda-2.6.20240714/candidate/changelog

Enjoy the Agda 2.7.0 RC 1 and please test as much as possible. Report problems and regressions to: https://github.com/agda/agda/issues

Finally online now -- the Wasm Research Day version of my weval talk, on partial evaluation for JS compilation, from last month. Fairly improved compared to the version I gave earlier. Still working on shipping this soon!

https://www.youtube.com/watch?v=_T3s6-C38JI&list=PLTxJmWeyp02DAOQnK1wHTo6KmfVAvAkme&index=11

My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!

Who? anyone who uses or has used an interactive theorem prover for whatever purpose What? 90 - 120 minute interviews (possibly including a small think-aloud programming session) When? interviews will be scheduled starting September 2024 Where? online (participants from anywhere are welcome)

We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.

Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy

#Agda #Coq #Lean #Isabelle #Usability #TheoremProvers

"What about an AutoClone trait?", take 57:

https://smallcultfollowing.com/babysteps/blog/2024/06/21/claim-auto-and-otherwise/

`Clone` today communicates behavior, not intent. Having a third trait besides `Clone` and `Copy` would let us actually differentiate between `Arc::clone` and `BigStruct::clone` at a glance, and remove the ceremony of the former when it makes sense.

#Rust #RustLang

Happy 12th Birthday to the funny little project that stole my name

I wrote a blog post about Agda Core! It's a bit long and not very polished, but I'm happy to have it finished (thanks to a long and distraction-free train ride to Swansea).

jesper.cx/posts/agda-core.html

#Agda #DependentTypes #Blog

Ferris says hi!

3D model by RayMarch (https://github.com/RayMarch/ferris3d).

#rustlang