Benki β†’ Bookmarks

β‡  previous page next page β‡’

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.

Bundler and test runner for Swift code compiled to WebAssembly.

I wish the Web did not need bundlers. Oh well.

Consolidates an Asciidoc file and all of its transitive includes into a single Asciidoc file.

Useful for places like GitHub, which do not support includes natively.

(I do wonder, however, if it isn’t sometimes preferable to just generate HTML each time you update your user manual and check that into your code repository or upload it someplace you can link toβ€”it is the universal language of the Web, after all.)

β‡  previous page next page β‡’