LHolten @LHolten@qoto.org

My rustacean friends are some of the craziest and most knowledgable Rust programmers around and that's just wild. I love seeing the crazy shit they're up to and learning from them.

I am absolutely overjoyed to announce the release of #KDL 2.0.0!! https://kdl.dev

It's a significant overhaul of the language to make it SO MUCH NICER in so many ways.

This is the culmination of over 3 years of work (4 if you count from before 1.0.0), by SCORES of contributors.

https://github.com/kdl-org/kdl/releases/tag/2.0.0

I want to give huge thanks to everyone who supported all of us through this, who jumped in and had some really amazing discussions weighing all sorts of interesting trade-offs.

The end result is absolutely not something any one person could've reasonably come up with.

I hope y'all enjoy it <3

As part of this release, several implementations have already launched with full support for v2.0.0, so you can try it now!

👉 #Rust #RustLang https://github.com/kdl-org/kdl-rs
👉 #C / #CPP / #Python https://github.com/tjol/ckdl
👉 #Elixir https://github.com/IceDragon200/kuddle
👉 #JavaScript / #TypeScript https://github.com/bgotink/kdl
👉 #Python https://github.com/tabatkins/kdlpy

KDL is already used in all sorts of projects, and by various folks as a DSL for their own small hobby things: https://github.com/kdl-org/kdl?tab=readme-ov-file#used-by

There are around 8k .kdl files out on GitHub, which is a lot considering it's usually a config language!

I fully expect this to be the last version of KDL ever released. We really really tried, but I don't think there's anything we can reasonably improve on.

From here on out, the language is in the (stable!) hands of the ecosystem.

Also, we're hoping to have GitHub syntax highlighting support soon!

(Boosts welcome!!)

I can't wait to see how people use default field values in #Rust!
It felt like an eternity to land this (specially if we count the years of discussion before the, I believe, 3rd RFC was accepted), but as of next nightly you will be able to write

struct Foo {
bar: Type = Type::const_method(),
}

Foo { .. } // implicit `bar: Type::const_method()` call

The main difference between https://github.com/rust-lang/rust/pull/129514 and derive(Default) is that the latter doesn't support having mandatory fields.
#RustLang

"TUIs should be minimal and practical" — but what if every single state change had a smooth transition effect (without JavaScript)?

Powered by @ratatui_rs and TachyonFX behind the scenes.

#rustlang #ratatui #tui

This was my tenth(!) year building 25 days of puzzles for #AdventOfCode. You can solve them all for free! Most people write code to solve them, but you can solve them however you like. I hope they help people become better programmers. 🌟

The first puzzle comes out in two hours: https://adventofcode.com/

I will never forgive #Rust #RustLang for that blanket From impl without having specialization yet. Absolutely soul crushing.

Nothing in the history of language design has so violently stifled progress and innovation in userland. Outrageous. Shameful.

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