This sounds very interesting. Do you have a reference?
Saw something like that once, couldn't find recently, sorry. Ask Peter?..
Readit Newsavmich commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evankhoury
avmich commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evankhoury
> to me it seems like high-level programming languages are already close to a specification language
They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many possible programs or even magical oracles that can do what a program does).
To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed.
Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.
avmich commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evankhoury
Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?
It's a bad reason. A lot of best practices are temporary blindnesses, comparable, in some sense, with supposed love to BASIC before or despite Dijkstra. So, yes, it's possible there is no good reason. Though I don't think it's the case here.
avmich commented on An Implementation of J (1992) jsoftware.com/ioj/ioj.htm... · Posted by u/ofalkaed
avmich commented on An Implementation of J (1992) jsoftware.com/ioj/ioj.htm... · Posted by u/ofalkaed
You don't really often need an array language, just like you don't really often need regexes.
When when you have a problem that perfectly fits the bill, they are very good at it.
The problem is they are terrible at everything else. I/O, data validation, manipulation strings, parsing, complex logic trees...
So I feel like just like regexes, there should be an array language parser embedded in most languages, that you opt in locally for just this little nudge.
In Python, it would be nice to be able to "import j" like you "import re" in the sdlib.
The entire J code base, including utility scripts, a console, a stdlib and a regex engine, is 3mb.
AFAIK APL was used to verify the design of IBM 360, finding some flaws. I wrote my first parser generator in J. I think these both contradict your opinion.
I think Iverson had a good idea growing language from math notation. Math operations often use one or few letters - log, sin, square, sign of sum or integral. Math is pretty generic, and I believe APL is generic as well.
avmich commented on When would you ever want bubblesort? (2023) buttondown.com/hillelwayn... · Posted by u/atan2
at a previous workplace, every new hire would discover the handwritten bubblesort in our codebase, freak out, and submit a pull request to fix it.
and every new hire got taken to the whiteboard to learn about sort algorithm performance: bubblesort is O(n) in the best case.
and in our codebase, the data being sorted fit that best case (the data was already sorted or almost sorted).
Not only in best case. Haven't seen this elsewhere, and know only few people who know that, so, a kind of a puzzle: what are the conditions when bubblesort is always O(n)?
avmich commented on When would you ever want bubblesort? (2023) buttondown.com/hillelwayn... · Posted by u/atan2
I recall "inventing" bubble sort during one of my first CS classes when the question was posed of how to sort a list. So, not that outlandish.
Agree. I remember the names of many of these algorithms, but not the logic.
avmich commented on What's the deal with Euler's identity? lcamtuf.substack.com/p/wh... · Posted by u/surprisetalk
This!
I've been posting the manifesto to friends and colleagues every tau day for the past ten years. Let's keep chipping away at it and eventually we won't obfuscate radians for our kids anymore.
Friends don't let friends use pi!
I wonder how many places we have in modern math symbols which we use for historical reasons, rather than because it's most convenient overall. I guess we are balancing things here.
avmich commented on Inflatable Space Stations worksinprogress.co/issue/... · Posted by u/bensouthwood
Usually, when we're interested in termination proofs, what we're really interested in is a proof that the algorithm makes constant progress that converges on a solution.