igornotarobot

5 ms·

1.
by igornotarobot 18d ago
You can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to rea
2.
by igornotarobot 2mo ago
The original departure time stays the same, and the delay is written separately. The same applies to trains. Well, this is how it usually works in Europe, not sure about other places.
3.
by igornotarobot 2mo ago
Of course, they have flight numbers, though the destination and the departure time was a good heuristic until it was not. I am much better at remembering the departure time than an arbitrary sequence of letters and numbers.
4.
by igornotarobot 2mo ago
How about two different planes departing to exactly the same destination at exactly the same time from two different terminals? That's how I missed my plane from Belgrade to Vienna. I have no other explanation but that they do it on pu
5.
by igornotarobot 3mo ago
If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find the
6.
by igornotarobot 7mo ago
I have fixed the target data structures and also make Claude compare the generated code against a python reference via PBT. However, the vibe-coded code generator stumbles upon a missed clone/copy case every now and then. This is where
7.
by igornotarobot 7mo ago
> I run into bugs all the time so it’s probably not ready for anyone other than me to use, but I’ve managed to go pretty deep (if not wide) in just a few days of work. Having similar experience with my experimental code generator to Rust
8.
by igornotarobot 9mo ago
Litex is probably closer to TLA+ than to Lean. Both draw inspiration from untyped set theory and LaTeX.
9.
by igornotarobot 10mo ago
> Just friendly remember that Open access publishing is the new business model that is more lucrative for publishing industry and it is basically a tax on research activities but paid to private entities and mostly paid by taxpayer money
10.
by igornotarobot 10mo ago
It probably will, but not the way we all imagine. What we see now is an attempt to recycle the interactive provers that took decades to develop. Writing code, experimenting with new ideas and getting feedback has always been a very slow pro
11.
by igornotarobot 10mo ago
Afaik, formal verification worked well for hardware because most of the things in hardware were deterministic and could be captured precisely. Most of the software these days is concurrent and distributed. Does the LLM + RL approach work fo
12.
by igornotarobot 10mo ago
This sounds amazing! What kind of systems take you a few hours to a few days now? Just curious whether it works in a niche (like sequential code), or does it work for concurrent and distributed systems as well?
13.
by igornotarobot 10mo ago
> TLA+ is not a silver bullet, and like all temporal logic, has constraints. > > You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on
14.
by igornotarobot 10mo ago
> TLA+ can specify anything that could be specified in mathematics. You are talking about the logic of TLA+, that is, its mathematical definition. No tool for TLA+ can handle all of mathematics at the moment. The language was designed fo
15.
by igornotarobot 10mo ago
TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof system that can automate s
16.
by igornotarobot 10mo ago
Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting control states for at least one input. After that, I t
17.
by igornotarobot 1y ago
It should be possible to write protocol specifications in Lean, e.g., this is a recent case study on specifying two-phase commit in Lean [1] and proving its safety [2]. However, there are no model checkers for Lean. Currently, you either ha
18.
by igornotarobot 2y ago
When you say peer reviews, do you mean academic publications or testimonials? I imagine it would be difficult to publish a paper at an academic conference proposing an alternative syntax for anything, even if it were better.
19.
by igornotarobot 2y ago
I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago was probably an exce
20.
by igornotarobot 6y ago
Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/ . And here
21.
by igornotarobot 6y ago
True. There are many frontends for Z3 that focus on various domains. For instance, those developed at Microsoft: - Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan... - Coral: https:/
22.
by igornotarobot 6y ago
> Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though. This
23.
by igornotarobot 6y ago
> Other examples would be checking liveness properties in the unbounded case, and possibly full Linear Temporal Logic, e.g., <>[]p ("eventually, property p is always satisfied"). I realize this is a tall order, but I thin
24.
by igornotarobot 6y ago
Just curious, what more complex properties do you like to be supported in Apalache? Many tools that are built on top of z3 are checking inductive invariants. By having a strong enough inductive invariant, you should be able to check safety.
25.
by igornotarobot 6y ago
Yes, it is weird. Now imagine. You learn English as a foreign language at school. You do a PhD and move for a postdoc to another country, say, Austria, because that's how academics do it. You work there, though you are not very motivat