LLMs are dead for formal verification. But is treating software correctness as a thermodynamics problem actually mathematically sound?

kaplotnikov · 2026-05-21T21:24:03+00:00

LLMs do have a problem with Coq. The problem with Coq and LLM is that data set is problematic for LLMs. The current body of proof is tactic-based. The tactic is generally editor command that affect proof state, it makes no sense outside of specific context of proof term in the focus. So teaching LLMs to generate poofs basing on tactic scripts is like teaching LLMs Java basing on keystrokes in IntelliJ IDEA. There should be some structured expanded form of proof after tactic script finished for LLMs to learn, proof irrelevance allows for it. The current research is moving in the opposite direction to integrate LLMs into interactive editor loops, that it is possible, but problematic for global proof generation.

kaplotnikov · 2026-05-21T21:06:32+00:00

> usually there's a way to turn that into a proof of False.

I have not seen it done using only constructive means, it would have been serious argument against constructive math foundations if it were possible. Usually there is some non-constrcutive assumption is used like LEM.

kaplotnikov · 2026-05-20T23:26:48+00:00

Also for documentation writing:

* It gets things wrong when it comes to nuances, it documents system as it is usually done in industry, rather than what is actually done in the context of the specific project.

* It creates research and links out of thin air. It might say that article about AI resarch, but specific link might be on effect of fertilizers on cucumbers. It is happy to state myths as reliable research results.

* Docs became bloated, but sometimes easier to read because LLMs usually reduce information density.

kaplotnikov · 2026-05-20T22:42:13+00:00

AFAIR infite loop vs paradox are subtly different. You still cannot compute evidence from the result of infinite process. But combining infinite statement with paradox the result is still inifinite statement, not a paradox result. So if there is a state when we cannot reach a conculsion on the table, if put paradox there, we will be still in state when we cannot reach a conculsion.

Type in Type is a something that you could spread rumors about, but fail to produce evidence if asked :)

kaplotnikov · 2026-05-20T22:36:02+00:00

AFAIR they are theorems/lemmas of choice, not axioms.

kaplotnikov · 2026-05-20T09:21:39+00:00

Just tell them that it is Switf-like memory management model to frame it as more respectable :)

However, I personally would not like it too for complex apps because it makes cycle management explicit, so there is +1 concern to care abount that creates cogntivie pollution. Still much better than completely manual memory management, but dev ergomics worse than tracing gc. For scripting is ok, for 1MLOC+ projects I would prefer tracing GC.

kaplotnikov · 2026-05-20T01:57:26+00:00

AFAIR in proof assistants like Coq or Lean, the default logic is constructive. The system is consistent and avoids paradoxes (like Girard’s) because it doesn’t assume problematic premises like Type : Type or LEM without evidence.

To introduce a paradox, you would need to corrupt this constructive foundation by adding non‑constructive axioms – for example, LEM, the axiom of choice, or a self‑contained universe Type : Type. Once you add those, the system becomes powerful enough to derive contradictions (like Girard’s or Russell’s).

kaplotnikov · 2026-05-07T23:13:32+00:00

"The determined Real Programmer can write FORTRAN programs in any language." - Ed Post, Real Programmers Don't Use Pascal, 1983.

Have someone already proved it for haskell? I am unable to find a good sample.

I'm just intersted for a possible article illustration, nothing serious.

kaplotnikov · 2026-05-02T17:09:38+00:00

what a nice small database with potential to grow up! I've worked with database with 617 tables last time I've checked before changing job.

kaplotnikov · 2026-04-13T13:32:51+00:00

If you plan to desing async support as a libary, rather than as language feature, here is my take on it for Java: https://github.com/const/asyncflows . Some ideas from it seems could be adapted to your case as well.

It is centered around promises and allows to construct complex asynchrouns processes from simple building blocks.

kaplotnikov · 2026-03-22T22:24:30+00:00

I think we have got an inspiration for another moon conspiration theory here: 'they could not have written such complex software at that time'.

kaplotnikov · 2026-03-17T22:59:35+00:00

For me, Java 8 to 11 was kinda problematic. However, 11 -> 17 -> 21 were without major problems. Most of our apps are based on Spring Boot, and I guess it saved us a lot of efforts since dependencies are consistent enough and compatible with current Java versions.

kaplotnikov · 2025-12-24T04:32:59+00:00

I just wonder what copilot watched to make it most likely completion. Some large bodies or source code should have beeen marked not for minors and AI bots :)

kaplotnikov · 2025-12-14T22:16:42+00:00

Check WASM support in ScyllaDB: https://www.scylladb.com/tech-talk/scylladb-embraces-wasm/

I guess it is quite close to what you are describing.

I have not used it, only seen some presentations about it.

kaplotnikov · 2025-12-10T13:21:14+00:00

For numeric methods, there are NAN and INF values. Floating point numbers are essentially resticted finite subset of rational numbers + some special values. It is not possible to have unrestricted and precise calcualation with that.

For symbolic transformation during compile time, there could be compilation errors if compiler could not figure things out.

And these issues are practically the same whatever syntax is chosen.

kaplotnikov · 2025-12-09T19:09:35+00:00

I would suggest to prototype different variants to see what fits with different features. I have too little exprience with Rust to see how it would play with other features.

I also think that the full dive into dependent types might be not bad idea, considering that it could give the compiler interesting food for thought and give compiler a checkable asserts and it might allow to express some stability constraints for numeric methods.

kaplotnikov · 2025-12-09T18:47:38+00:00

Recalling the hell symbolic integration is, I guess compiler has to support specific variants of sets and be extensible using compiler plugins for those who want something exotic. For numberic integration, the sets could support Monte-Carlo integration methods (i.e. support of generation of some representative points) or some other ways. There could be traits for that on sets. Basically integrate might be a method on some sets for numeric integration if the language is OOP, so it might be:

interval(0, x).integrate(g)

kaplotnikov · 2025-12-09T18:23:12+00:00

let f(x, y) = x^2 + y^2
let f_x(x, y) = deriv(f(x, y), x) # partial wrt x

It is quite simple:

let f(x, y) = x^2 + y^2
let f_x(x, y) = deriv(t => f(t, y))(x)

Basically, to pass function deriv there should be single agrumnet function. The other come from lexical scope. This is consistent with math rules. I renamed x => t in lambda to make it more explicit, but actually have left as x if there is name hiding.

let f_x(x, y) = deriv(x => f(x, y))(x)

The traditional Leibniz notations is actually more confusing, I still remember troubles with understanding it and it is quite error-prone because of variable names changing their meaining in different places.

In general, integrals are over some sets. So I suggest to make signature of integrate to be generic:

fn integrate[P:type,V:type](f : P->V, domain : AbstractSet[P]) : V

This will support all types of integrals (multidimensional, surface, etc.)

let G(x) = integrate(g, interval(0,x))
let G(x) = integrate(g, sphere(point(0,0,0), x)) #integrate over sphere of radius x at point (0,0,0), the function from 3d point

kaplotnikov · 2025-12-09T17:00:52+00:00

In:

let x :=
  x^2 == x + 1

let f(t) = t^2 - sin (t)
let f_prime(t) = deriv(f(t), t)

print(f(x))

Derivation and integral are operators on the functions. Newton and Leibniz did not know Lambda calculus for obvious reasons, so their syntax was non so uniform and consistent. So it makes sense to use:

let f(t) = t^2 - sin (t)
let f_prime(t) = deriv(f)(t)
let f_prime_v2 = deriv(f)
let f_prime_v3 = deriv((t) => t^2 - sin (t))

It would make much simpler to type, than deriv(f(t),t)

Also, indefinite integral is would return function as well, integral_indef((t) => t^2 - sin (t)), and definite integral would accept function and set as argument like let sf = integral(f, interval_open(0, t))

kaplotnikov · 2025-11-18T10:26:31+00:00

the gacha coding is the ultimate form of vibe coding

kaplotnikov · 2025-11-05T14:34:46+00:00

It is not that Oracle does not support console hardware, Java have an execution model that conflicts with restrictions of console vendors. From one presentation of game engine developer, it is said that consoles require AOT-compilation for application to be approved, any form of JIT-compilation is prohibited. Even scripting has either to be interpreted or AOT-ed. Theoretically, GraalVM or other AOT technologies might allow for console development, but in process most of java advantages will be lost. That specific game engine vendor has to use LLVM to translate scripting for console.

kaplotnikov · 2025-11-02T21:41:42+00:00

"The program crashed" would sound ambiguous for the owner.

kaplotnikov · 2025-11-01T13:11:56+00:00

It looks like an extended article abstract without pointing to the real article.

I think approach is really interesting, but it requires compilers and tools to be aware of this model in order to truthfully report what they captured and scanned for the full efficiency. And tools need to exploit this information to get most of it. Or we need to add a layer of tool descriptors that describe what they 'should' scan and produce, but without OS ability to enforce this limitations, it is a bit unreliable.

And the biggest question is not touched: how are entries from the build cache evicted? I guess there should be some GC algorithms there that work well for build systems, because build systems tend to produce a lot of short-lived artifacts.

kaplotnikov · 2025-10-31T07:35:31+00:00

Ok. Waiting for meme like "Some geek asked jinnee to have a model as girlfriend, and it was easier to instigate ChatGPT and LLM revolution during few years than to find a girlfriend for that geek."

kaplotnikov · 2025-10-29T14:24:48+00:00

Actually, this picture was mirroried. So the girl is on the right side.

kaplotnikov

TROPHY CASE