It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.
However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.
Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.
I am not sure I agree we've yet to see any other architecture that competes with a large transformer. For example, in long-range tasks such as those related to genome prediction, state-space models (Mamba) exhibit SOTA performance. I also think it's hard to separate architectural advantages from maturity, given that transformers have received much more attention.
I agree. I also think it's about the hardware and, obviously, recognizing AD as the fundamental primitive.
Particular architectures don't matter so much yet. It's quite possible that S3-Mamba or xLSTM could be used in lieu of transformers and we would still have LLMs.
I would say that lots of interesting things are happening in biotech, and these things are slowly building critical mass, similar to what happened in computer hardware during the period 1970-2000.
Genomic platforms are now able to capture multiple measurements (e.g. RNA and chromatin openness) from single cells in large tissue slices/massive perturbation experiments.
Once time gets baked into the equation, we will be able to build better models of systems biology. However, human trials will still be a major bottleneck.
It is difficult. I think the key is that Spain has a large corps of civil engineers working for the government. They plan all projects with great detail and then oversee their execution.
Agile regulations against NIMBYism and a world-class civil engineering industry with HQs in Madrid also help.
A good analogy is to ask what would need to be true for Madrid to replicate the AI hub in SF? Great VC, top engineers, certain risk-taking mentality, etc.
So, it's not easy. The environment that creates a fabric for radical innovation is quite different from a statist mentality, although hopefully, both are not mutually exclusive.
I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs.
TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future.
My statement obviously referred to major cities, which is where most IT jobs are, as I indicated remote work allows you to leverage cheaper locations.
Take for example Oxford. A typical rental will be around £1,600 pcm. The median pre-tax salary is around £50,000, which converts to around £3,100 net. So, the apartment is actually more than 50% of your net income. Some programming jobs will pay a bit more, but you get the idea.
Another example, in Barcelona, a median net salary is less than a median rental. IT will pay better, but expect to spend around 40% of your net salary. I could also bring up Stockholm or Copenhagen and, unless you are in very senior IT jobs, it's going to look very similar.
True, there's also another factor about not having to be tied to a geographic spot, housing costs.
In EU, even relatively good IT salaries are mediocre when you factor in monthly rental. A simple one-bed apartment can easily take 50% of your net income.
Having freedom to move, even within a particular country, allows reducing that 50% to something more sustainable.
But, if I have understood correctly on a quick read, they also claim transformers have pretty low expressive power. In particular, they claim they are limited to star-free subregular languages, whereas RNNs can recognize any regular language/simulate finite automata.
This doesn't imply you can't get aid from a LLM to e.g. implement a function that has a formal specification (an application I think is very promising), but surely it has some profound implications on how much of a large system can be understood by a LLM at once, without supervision.
Oxford, UK