cross-posted from: https://programming.dev/post/37407248

Scrolling through this webpage is an adventure.

Scrolling through this webpage is an adventure.

cross-posted from: https://programming.dev/post/36983916

Freund wasn’t looking for a backdoor when he noticed SSH connections to his Debian testing system taking 500 milliseconds longer than usual. As a database engineer benchmarking PostgreSQL performance, he initially dismissed the anomaly. But the engineer’s curiosity persisted.

The backdoor’s technical sophistication was breathtaking. Hidden across multiple stages, from modified build scripts that only activated under specific conditions to obfuscated binary payloads concealed in test files, the attack hijacked SSH authentication through an intricate chain of library dependencies. When triggered, it would grant the attacker complete remote access to any targeted system, bypassing all authentication and leaving no trace in logs.

The backdoored versions 5.6.0 and 5.6.1 had been released in February and March 2024, infiltrating development versions of Fedora, Debian, openSUSE, and Arch Linux. Ubuntu’s upcoming 24.04 LTS release, which would have deployed to millions of production systems, was mere weeks away.

The technical backdoor was merely the final act of a three-year psychological operation that began not with code, but with studying a vulnerable human being.

Explores how the Lean programming language handles 2 + 2 = 4, which other programming languages collapse into a bool, but Lean considers a Proposition, and requires Proof.

How does provably correct programming look? This article seems to give a good introduction and example.

Explores how the Lean programming language handles 2 + 2 = 4, which other programming languages collapse into a bool, but Lean considers a Proposition, and requires Proof.

How does provably correct programming look? This article seems to give a good introduction and example.

Pike is a dynamic programming language with a syntax similar to Java and C. It is simple to learn, does not require long compilation passes and has powerful built-in data types allowing simple and really fast data manipulation.

int getDex()
{
  int oldDex = Dex;
  Dex = 0;
  return oldDex;
}

private void
show_user(int|string id, void|string full_name)
{
  write("Id: " + id + "\n");
  if (full_name)
    write("Full name: " + full_name + "\n");
}

The Go 1.18 release introduced generics and with that a number of new features, including type parameters, type constraints, and new concepts such as type sets. It also introduced the notion of a core type. While the former provide concrete new functionality, a core type is an abstract construct that was introduced for expediency and to simplify dealing with generic operands (operands whose types are type parameters). In the Go compiler, code that in the past relied on the underlying type of an operand, now instead had to call a function computing the operand’s core type. In the language spec, in many places we just needed to replace “underlying type” with “core type”. What’s not to like?

Quite a few things, as it turns out! To understand how we got here, it’s useful to briefly revisit how type parameters and type constraints work.

For the Go 1.25 release (August 2025) we decided to remove the notion of core types from the language spec in favor of explicit (and equivalent!) prose where needed. This has multiple benefits: …

However, there are some important features that WinSock just doesn’t expose. […]

Rust’s current async ecosystem is built atop a particularly cursed concept. It’s an unstable, undocumented Windows feature. It’s the lynchpin of not only the Rust ecosystem, but the JavaScript one as well. It’s controversial. It’s efficient. […] Without it, it’s unlikely that the async ecosystem would exist in its current form. It’s called \Device\Afd, and I’m tired of no one talking about it.

However, there are some important features that WinSock just doesn’t expose. […]

Rust’s current async ecosystem is built atop a particularly cursed concept. It’s an unstable, undocumented Windows feature. It’s the lynchpin of not only the Rust ecosystem, but the JavaScript one as well. It’s controversial. It’s efficient. […] Without it, it’s unlikely that the async ecosystem would exist in its current form. It’s called \Device\Afd, and I’m tired of no one talking about it.

Seed7 is a general purpose programming language designed by Thomas Mertes. It is a higher level language compared to Ada, C/C++ and Java. The Seed7 interpreter and the example programs are open-source software. There is also an open-source Seed7 compiler. The compiler translates Seed7 programs to C programs which are subsequently compiled to machine code.

In Seed7 new statements and operators can be declared easily. Functions with type results and type parameters are more elegant than a template or generics concept. Object orientation is used where it brings advantages and not in places where other solutions are more obvious. Seed7 contains several concepts from Pascal, Ada, C, C++ and Java.

• Seed7 Website
• Seed7 Source on GitHub
• FAQ
• “Screenshots” - example programs with linked source, some web-runnable

The author posted on Reddit; quoting in part:

Seed7 is based on ideas from my diploma and doctoral theses about an extensible programming language (1984 and 1986). In 1989 development began on an interpreter and in 2005 the project was released as open source. Since then it is improved on a regular basis.

Seed7 is about readability, portability, performance and memory safety. There is an automatic memory management, but there is no garbage collection process, that interrupts normal processing. The templates and generics of Seed7 don't need special syntax. They are just normal functions, which are executed at compile-time.

Seed7 is an extensible programming language. The syntax and semantics of statements (and abstract data types, etc.) is defined in libraries. The whole language is defined in the library "seed7_05.s7i". You can extend the language syntactically and semantically (introduce new loops, etc.). In other languages the syntax and semantics of the language is hard-coded in the compiler.

Seed7 checks for integer overflow. You either get the correct result or an OVERFLOW_ERROR is raised. Unlike many JVM based languages Seed7 compiles to machine code ahead of time (GRAAL works ahead of time but it struggles with reflection). Unlike many systems languages (except Rust) Seed7 is a memory safe language.

Some programs written in Seed7 are:

• make7: a make utility.
• bas7: a BASIC interpreter.
• pv7: a Picture Viewer for BMP, GIF, ICO, JPEG, PBM, PGM, PNG, PPM and TIFF files.
• tar7: a tar archiving utility.
• ftp7: an FTP Internet file transfer program.
• comanche: a simple web server for static HTML pages and CGI programs.

Code Example

# Print a Fahrenheit-Celsius table with floating point numbers.

$ include "seed7_05.s7i";  # This must be included first.
  include "float.s7i";     # Subsequent includes do not need a $.

const proc: main is func
  local
    const integer: lower is 0;
    const integer: upper is 300;
    const integer: increment is 20;
    var integer: fahr is 0;
    var float: celsius is 0.0;
  begin
    for fahr range lower to upper step increment do
      celsius := float(5 * (fahr - 32)) / 9.0;
      writeln(fahr lpad 3 <& " " <& celsius digits 2 lpad 6);
    end for;
  end func;