rafaelRiv

I still do diagrams. Not UML specifically, but using mermaid.js. It is a great way to think about the requirements before coding

> When was the last time you ..or anyone.. reviewed the assembly language or binary output of your compiler?

not even a week ago. But generally people prefer to burn millions on compute instead of seeing the output of the compiler and see how they can optimise their code

> Not many people are such cowboys today.

Now-day, it is the llm that write tests. Nobody look at it and verify if it is meaningful. If the test pass, ship it.

It still cowboys days

It is super laughable when you read his github bio. I had a good laugh not ngl

Not only that. Citing "What doesn't kill you make me stronger" in this context is very ironic as Nietzsche was talking for himself. He took that from Ralph Waldo Emerson while stripping the moral aspect of it

it is not because it work that it is good. It still need to be maintained and this is a huge deal

That is magic thinking and even religious

That is why I prefer correct by construction instead of relying on proofs

This is my experience with llm and all dependent type language like idris2

I do a lot of software dev with idris2 in my free time and this is the problem. Everytime I try llms with formal verification, llms tend to try to remove all type check and cheat. That is why I am soooo sceptical of people using lean will llm too .

> we coder-stonemasons spent our days meticulously carving code-stone into finished pieces

In what world this was ever true ? a software or a lib is pretty much never finished

It can create very bad one. Wake me up when it will make subtensial progress on Cubical Type Theory

Anything I don't agree is pasted from an LLM

> For example, I predicted about 15 years ago that AI would decisively beat humans at math, because math is formalizable. Most people didn't believe it until this summer, and some don't believe it still.

That is a laughable quote for anyone that know the history of type theory and the foundational crisis that happened at the beginning of the last century. Math as a whole can't be formalizable but we can create various formalist for different math purpose just like we have so much programming languages.

And the study and the creation of those formalisms is not something automatisable.

> NFTs literally were mass psychosis

LOL as if AI was a not a mass psychosis ... "AI have 10% of kill us all"