But for any important code the only way to know that it's correct is to hand-audit every line, which is harder than writing every line because this allows you to build a conceptual hierarchy and model within which you can think about the code.

So there's a fundamental limit to the speedup from LLMs when writing anything you care about.

(The main objection will be what about when you have a human engineer working on your behalf. But this is a distraction: sometimes you can fully trust an engineer, which is not at all true for LLMs.)

Comments URL: https://news.ycombinator.com/item?id=48278179

Points: 6

# Comments: 4

subligence /sʌbˈlɪdʒəns/ n.

A lesser or rudimentary form of intelligence; the capacity to respond, select, or adapt without full understanding. The semblance of mind in animals, machines, systems, or inanimate things. Discernment beneath reason; inferior intelligence.

Example: "Since December, the coding models have gotten noticeably more subligent, so much so that the undiscerning eye has trouble distinguishing their output from human intelligence."

Comments URL: https://news.ycombinator.com/item?id=48234818

Points: 4

# Comments: 6

Although many newer languages are safer (with the exclusion of Rust, primarily by being slower) the same kinds of issues that are there in C are there in these languages, their effects are just harder to see.

People complain about C as though they know how to fix it.

Comments URL: https://news.ycombinator.com/item?id=46511120

Points: 3

# Comments: 1

We're working on Xr0 [0] and have been building a static-site generator that meets our tastes and needs. The basic emphasis is on simplicity and content rather than customisability and feature-richness. We are imitating Jekyll and Hugo (and other SSGs) in their basic generation paradigm and LaTeX in its separating form from content, but attempting to combine these into a unified, minimal philosophy where you can open a repo and start writing without needing a CLI tool to generate your folder for you.

The project is broken into two applications: an SSG you can run locally (or in a GH Action etc.) and a platform for easy hosting that bundles in some basic audience interaction features. Both are available on GitHub: [1] and [2].

We've been working on this somewhat sporadically for the past couple of months, and it is very much a WIP, particularly in the themes it offers, but we're keen to hear thoughts on this.

[0]: https://xr0.dev

[1]: https://github.com/hyloblog/hyloblog

[2]: https://github.com/hyloblog/hyloblog-ssg

Comments URL: https://news.ycombinator.com/item?id=42986330

Points: 3

# Comments: 0

  if (x > 0) {
    /* code */
  } else {
    /* more code */
  }

Xr0 is a work in progress, and we'll get there step-by-step.

So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.

> It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.

True. As you said earlier:

> The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.

This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.

If the program's safety depends on the semantics of C and how they've been used in a function, it will be possible to deal with all the conditions upon which a program could be unsafe (in the sense of the standard safety vulnerabilities – like those listed here [0]). Doing so would lead to denouement, so that the annotation to the main function would be empty (meaning none of those bugs can occur).

Programs that might be unsafe should not be verifiable.

[0]: https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...

However, the main reason why this argument is flawed is it omits the heart of the matter: the annotations. Xr0 empowers programmers to propagate safety semantics. A program that is only safe if the Collatz conjecture holds is (surprise) only safe if the Collatz conjecture holds. So in Xr0 the only requirement we would impose is that this program be augmented with an annotation that communicates that it is only safe if the Collatz conjecture is true.

So the flaw in the reasoning is we haven't claimed that Xr0 can prove arbitrary programs are safe. We've claimed that Xr0 can prove the correspondence between the safety semantics denoted in an annotation and a function body. Above there are no annotations given which would specify "this program is safe only if the Collatz conjecture is true". It shouldn't be hard to prove the correspondence between such an annotation and the program you've written, e.g.:

    def main(): ~ [
        buffer = [0, 0, 0, 0, 0]
        x = int(input())
        if x >= 1:
            collatz_cycle_element = cycle(collatz, x)
            print(buffer[collatz_cycle_element])
    ]

        buffer = [0, 0, 0, 0, 0]
        x = int(input())
        if x >= 1:
            collatz_cycle_element = cycle(collatz, x)
            print(buffer[collatz_cycle_element])

Literally on the website. The purpose of the prototype is to show the feasibility of the approach we've taken, not to work on whole programs.