Benki → Bookmarks

next page ⇢

Lazy dynamic constants for Java. Implemented as dynamic constant pool entries.

Given that a significant part of the startup time of a typical Java application is taken up by class initialization, I wonder if this could be used for good effect when declaring the ubiquitous Logger instance and such.

A more verbose alternative that works without this is:

private static Logger logger() {
  class Statics {
    static final Logger logger = Logger.getLogger(Parent.class);

  return Statics.logger;

As the Dycon README points out, this alternative (which is a variant of the initialization-on-demand holder idiom) incurs overhead in the form of an additional class object, so it has its drawbacks. Still, you may prefer it because it does not involve bytecode trickery.

GTK 3 and GTK 4 bindings for Swift. Autogenerated, for the most part, based on GObject Introspection.

Checks cross-references of files and directories in readmes and other documentation. Meant to be used as part of a continuous integration pipeline.

Installs executable Swift packages from their source code repositories.

Converts the output of makefiles into TAP format, which can then be piped into any TAP formatter. There are TAP formatters that produce quite pretty output.

Programming language built with subtyping (lattice typing) and categorical duality in mind. The core of the language is a term language for sequent calculus (rather than natural deduction as is typical for functional languages).

The general sentiment of people in the know appears to be:

  • Lean 4 is a nice programming language, more ergonomic and easier to learn than Haskell or Idris in many ways. For example, monadic code looks more like Rust than Haskell.
  • Given the design choices the language designers made, the implementation could, in time, be made efficient enough to compete with the likes of C and Rust. For example, in-place mutation of collections and data structures is easy to accomplish.
  • The tooling and in particular the integration with Visual Studio Code is top-notch.
  • The ecosystem and community around Lean 4 as a programming language (as opposed to as a theorem prover) is very small at the moment.

I would add:

  • The Lean ecosystem (Mathlib in particular) making use of classical as well as intuitionistic logic has the potential to make theorem proving significantly more palatable than many competing systems.
next page ⇢