Item — HN Reader

> would be an issue even if it were humans writing

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.

1 comments

I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect.

For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that works for most realistic cases, e.g. integers -> Int64. Other types become considerably more irritating; you might prove something with regards to all real numbers, but when exporting to a "real" programming language, there really isn't such thing as "real" numbers, since computers can really only do the rationals. You could export to float64, but then you're dealing with IEEE rounding, which may or may not be fine for what you're working on. You could use something like GMP (which is what I ended up doing when I had this issue) but of course you pay a performance penalty by doing that, and of course you're then trusting the correctness of GMP (though there is a verified subset, to be fair).

I feel like with TLA+, I am typically working on higher-level problems. Usually I'm modeling distributed systems, which sort of inherently requires an "opinion" for deployment.

How would I deploy this code? Erlang? Kubernetes? Docker Swarm?

How am I doing service discovery? DNS? YOLOing with raw IP addresses?

Suppose my model has a global function [1] that I'm writing to as a global shared store? Where does this live? Is this a local cache? Is this Redis? Memcached?

I could go on. The whole point of TLA+ is to write and test the algorithms, and very purposefully allows and encourages you to ignore details that aren't necessary to show correctness of your algorithm.

I'm not saying you couldn't do this, to be clear. You could absolutely create an exporter for TLA+, but my point is that it would require a good chunk of opinions and decisions to do it. You'd also need to ensure that the semantics of these things properly map to your model, else the exporter is only of debatable utility.

I think this is why there isn't really a serious exporter for TLA+. You just work at a different level with it, and I think there are just too many (kind of arbitrary) decisions that would have to be made in order to do anything useful.

[1] In TLA+, "function" basically means key-value map.

That's illuminating, thank you for a generous reply. The point about real numbers and their representation (or lack thereof) in programming languages is a great example of the gulf between mathematics and programming. I understand that for most languages, there can be no direct correspondence between a mathematical proof and the program that implements 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...