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.
Similar to the Swift Package Index, but using a stateful database rather than a JSON index file in a public Git repository as a source of packages.
Is written in JavaScript and integrates tightly with GitHub.
A small x86 retrocomputer.
Of course one could write a list like this in the other direction, too. I still find it interesting because I am not very familiar with Swift.
Bundler and test runner for Swift code compiled to WebAssembly.
I wish the Web did not need bundlers. Oh well.
SwiftUI-inspired GTK 3 wrapper.
Compatible SwiftUI clone that targets WebAssembly.
Sources a big JSON list.
The service is written in Swift itself.
The way Swift does this sounds really appealing for small devices.
Matthias
#
NTRU in OpenSSH
OpenSSH has supported post-quantum cryptography for several years now. sntrup761x25519-sha512@openssh.com (hybrid Streamlined NTRU Prime and X25519) was introduced in OpenSSH 8.5. It was made the default key exchange mechanism in OpenSSH 9.0.
The reason it is a hybrid mechanism is that the security of NTRU is not as well-established as that of X25519 and other classical methods.
Note that this for key exchange, not authentication. But considering that post-quantum cryptanalysis is a future concern rather than one situated in the present, that is what is worth focusing on right now. After all, someone who can break your key exchange in the future can record your encrypted exchanges now and decode them later. But they cannot travel back into the past to impersonate you in the present.
Haskell prelude replacement by Serokell.
Links Linux ELF binaries against Windows PE/COFF DLLs.
Generates HTML from Asciidoc and uploads it as the README for a SourceHut repository.
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.)
Browses UIs on Macs, facilitating their scripting via AppleScript.
Platform for interactive documents inspired by HyperCard.