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

Points: 3

# Comments: 0

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

Points: 1

# Comments: 0

Computational Substrates: How Well-formed, Self-replicating Programs Emerge from Simple Interaction - https://arxiv.org/abs/2406.19108

Brainfuck, Forth, Subleq, and most recently Z80 assembly programs with mutations, interactions, and self-modification. Z80 has an LDIR instruction that copies a block of data from one location in memory to another, which allows the "organisms" to reach/discover reproduction quicker and more reliably in repeated experiments. As soon as that happens, it inevitably takes over the "world".

Hm, sounds more like "Lord of the Flies" than Rings.

Nobody is qualified to judge the usefulness of mathematical, scientific, artistic, or any other kind of research that people choose to dedicate their time doing. And the world is better for it.

> or representative of reality

This so-called "reality" you speak of is some arbitrary representation in your head. It's your theory and patterns of abstraction, as you call it. Who knows how far or close you are to "objective" reality, whose existence we can only know through representations and abstractions. Mathematics and logic are some of the best tools we have of getting closer to that truth and understanding. All the sciences and even some of the arts are based on it.

In a recent discussion about the paper "How real are real numbers?" by G. J. Chaitin, someone mentioned that there seems to be a trend of a "computational" approach to mathematics on one hand, and from the other side, a "mathematization" of computer programming. With the rise of language models and their ability to generate correct programs, I imagine there is a pressing need to bridge the gulf between the two fields. Not only to verify the correctness of programs written in existing languages, but to design languages where that need for verification is taken into considertaion from the ground up, maybe close to Rust where the compiler refuses to compile a program that cannot be verified to be correct.

A common complaint about software engineering is that it is not "engineering" as a formal discipline; and about computer science that it is not a "science" (nor is it about computers, any more than astronomy is "telescope science" and biology is "microscope science" [^1]). It seems to me that a firmer grounding in mathematics, particularly in programming language design, would be helpful in improving the situation, so that software is actually "engineered" based on immutable truths and logic, and verified to be correct.

And how would the computational approach to mathematics influence it as a discipline.. Perhaps it may bring the field closer to a "science" with more experimental exploration.

[^1]: I think attributed to Vinton Cerf in _Where Is the Science in Computer Science?_. https://cacm.acm.org/opinion/where-is-the-science-in-compute...

I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.

From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.

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

Points: 1

# Comments: 0

That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs.

Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?

That's beautiful. Here's the Git repo with implementation.

https://gitlab.inria.fr/core-math/core-math/-/blob/master/RE...

JavaScript

    const eml = (x, y) => Math.exp(x) - Math.log(y);
    const emlLn = (x) => eml(1, eml(eml(1, x), 1));
    const emlMul = (x, y) => eml(emlLn(x) + emlLn(y), 1);
    const emlAdd = (x, y) => emlLn(eml(x, 1) * eml(y, 1));

    import math

    def eml(x, y):
        return math.exp(x) - math.log(y)
    def eml_ln(x):
        return eml(1, eml(eml(1, x), 1))
    def eml_mul(x, y):
        return eml(eml_ln(x) + eml_ln(y), 1)
    def eml_add(x, y):
        return eml_ln(eml(x, 1) * eml(y, 1))

    function eml(float $x, float $y): float {
        return exp($x) - log($y);
    }
    function eml_ln(float $x): float {
        return eml(1, eml(eml(1, $x), 1));
    }
    function eml_mul(float $x, float $y): float {
        return eml(eml_ln($x) + eml_ln($y), 1);
    }
    function eml_add(float $x, float $y): float {
        return eml_ln(eml($x, 1) * eml($y, 1));
    }

    func eml(x, y float64) float64 {
        return math.Exp(x) - math.Log(y)
    }
    func emlLn(x float64) float64 {
        return eml(1, eml(eml(1, x), 1))
    }
    func emlMul(x, y float64) float64 {
        return eml(emlLn(x)+emlLn(y), 1)
    }
    func emlAdd(x, y float64) float64 {
        return emlLn(eml(x, 1) * eml(y, 1))
    }

    fn eml(x: f64, y: f64) -> f64 {
        x.exp() - y.ln()
    }   
    fn eml_ln(x: f64) -> f64 {
        eml(1.0, eml(eml(1.0, x), 1.0))
    }
    fn eml_mul(x: f64, y: f64) -> f64 {
        eml(eml_ln(x) + eml_ln(y), 1.0)
    }
    fn eml_add(x: f64, y: f64) -> f64 {
        eml_ln(eml(x, 1.0) * eml(y, 1.0))
    }

    local math = require("math")

    function eml(x, y)
        return math.exp(x) - math.log(y)
    end
    function eml_ln(x)
        return eml(1, eml(eml(1, x), 1))
    end
    function eml_mul(x, y)
        return eml(eml_ln(x) + eml_ln(y), 1)
    end
    function eml_add(x, y)
        return eml_ln(eml(x, 1) * eml(y, 1))
    end

[^1]: https://lilting.ch/en/articles/eml-single-operator-elementar...

Charles Bukowski, William Burroughs, and the Computer - https://realitystudio.org/bibliographic-bunker/charles-bukow...

> Why should we believe in real numbers, if most of them, it turns out,[^15] are maximally unknowable like Ω? [^16]

The footnotes:

> [^15]: See the chapter entitled The Labyrinth of the Continuum in [Chaitin, 2005]

> [^16]: In spite of the fact that most individual real numbers will forever escape us, the notion of an arbitrary real has beautiful mathematical properties and is a concept that helps us to organize and understand the real world. Individual concepts in a theory do not need to have concrete meaning on their own; it is enough if the theory as a whole can be compared with the results of experiments.

---

The reference [Chaitin, 2005] in footnote 15 links to..

Meta Math! The Quest for Omega - http://arxiv.org/abs/math/0404335

> This book presents a personal account of the mathematics and metamathematics of the 20th century leading up to the discovery of the halting probability Omega. The emphasis is on history of ideas and philosophical implications.

Irreducible Complexity in Pure Mathematics - http://arxiv.org/abs/math/0411091

> By using ideas on complexity and randomness originally suggested by the mathematician-philosopher Gottfried Leibniz in 1686, the modern theory of algorithmic information is able to show that there can never be a "theory of everything" for all of mathematics.