Agingcoder

That’s what they do usually I understand - llm generates proof in lean, and proof checker proves.

A couple of days ago a colleague of mine was talking about very old rts games he still liked to play , and mentioned red alert. It turned out he had never heard of dune 2, Warcraft 1 and 2!

It has a very large number of bugs.

My favourite one ( still happens ) is having to mute then unmute at the beginning of the conversation otherwise nobody can hear me. It was so common, with people fiddling with their headset, calling again etc that I eventually asked everyone exhibiting audio issues to start with this

Another interesting one is that if you’re not connected properly , you send messages , but never get notified that they never left, and are never notified that you’re not connected.

It’s also a resource hog and will eat your machine for breakfast.

The list goes on and on, it’s very surprising.

This one made me laugh , thanks ! I wish there was some kind of slashdot like ´funny’ tag

Full screen video ads on the home screen ? I don’t see this on mine.

It also can’t stream games

No it’s vastly different - give it a try first . Reverse debugging with full dataflow is magical. Interestingly enough, it takes a while to get to used to it since you tend to do things the old way, when the Pernosco, science fiction way is much better and actually works

Pernosco

Blows everything else out of the water.

https://pernos.co/ ( I’m not affiliated to them in any way, just a happy customer)

Several things : immediately after 2008 less demand for exotics because clients were afraid of them, cutting costs rather than increasing revenue ( that’s industrialization with IT and standardization ) and more importantly, industry reaching some kind of maturity, with large quant libraries which are pretty stable these days.

Im reasonably familiar with the exotics quant space.

It’s essentially IT/data work - the days of sophisticated maths are mostly gone. There always was a lot of code, but these days for most people there’s little to no new maths.

From what I’ve seen, post-2008 the job changed significantly, with more IT, less maths, more standardization - basically the job moved from bespoke everything to super industrialized. You’ll be able to have your model work for one underlying and one product, but what’s really useful is for lots of underlyings and many products - and that’s very hard.

That being said, and that’s important, you must understand the maths behind, otherwise you won’t be able to do anything useful.

These days a single machine with lots of ram and cores will handle almost everything you throw at it, barring specific compute intensive / memory bound scenarios ( current AI, gaming etc ).

Same issue with apple car. ‘ hey Siri, please play ‘call your girlfriend’ on Spotify by (artist)’

‘Sorry I don’t know anyone called ‘your girlfriend’’ The kids find it hilarious

Is the same mechanism at play with football ? Say Real Madrid gets so much money from champions league that they can buy all the best players and then keep winning ? And then only a small clique of elite clubs end up winning all the time?

( disclaimer : I know nothing about football !)

That’s what struck me immediately - these are all typical tricks from the 90s. I remember demos ( I think complex/dope in 95) where the awesome ‘real time reflections’ where actually an animated texture. I was quite impressed when someone explained the trick.

Looks like typical demo scene tricks applied to gaming

This is pretty standard ( or at least used to be 20 years ago ) in high performance chess programming, see

https://www.chessprogramming.org/Bitboards

https://healeycodes.com/visualizing-chess-bitboards

This is weird - my mother very rarely drinks but she’ll be hard pressed telling you exactly when was the last time time . This doesn’t make her an alcoholic.

Or should you start the rule with ‘you’ve been drinking everyday for a while’?

Computer architecture a quantitative approach by Patterson and hennessy

It’s the real life exchange rate for algorithms and data structures. Basically understanding your infrastructure and its performance characteristics will help you design simpler ( and therefore better )systems

I used mplayer ( the ancestor to mpv as I’ve just realized ) in the early 2000s which I think could handle everything under the sun back then.

Cloudflare, google project zero.

This is a truly remarkable book, and a must read for any engineer who depends on a gc . And if you don’t need a gc, the book starts by talking about allocators, which are actually very important too !

It’s pretty standard in many places I think - the point here is not the null gc but rather exact memory requirements being proved statically.

I liked window maker and enlightenment, both of a which appeared a bit later.

This title is very hard to parse

It’s also not a solved problem unlike what the article claims, unless ‘solved’ doesn’t mean ‘works all the time ‘.

Very nice post thanks - I didn’t know about cakeml and bootstrapping formally verified compilers.

Which are both systems with a fair amount of theory behind them !

They can actually - I thought they couldn’t , but the latest ones can, much to my surprise.

I changed my mind after playing with cursor 2 ( cursor 1 had lasted all of 10 mins), which actually wrote a full blown app with documentation, tests , coverage, ci/cd, etc. I was able to have it find a bug I encountered when using the app - it literally ran the code, inserted extra logs, grepped the logs , found the bug and fixed it.

> One objection I hear a lot is that LLMs are only good at greenfield projects. I'd push back hard on this. I've spent plenty of time trying to understand 3-year-old+ codebases where everyone who wrote it has left.

Where I am, 3 year old is greenfield, and old and large is 20 years old and has 8million lines of nasty c++. I’ll have to wait a bit more I think …

In my experience codex fails at that kind of task in many cases.

I think it’s unlikely it will succeed at that task with a real world , old, large codebase.

Now, the next release might work !