nudpiedo

And the word from arabic comes, for both of them comes from persian for hte term lapis lazuli (lāžward) and suposedly this comes from sanskrit... but I ignore how it may sound in sanskrit.

In this case it does by hitting hardware maximum. It scales until the max it is possible, due the bottleneck being in the hardware, not in the database or i/o. Check the article again:

> At maximum throughput, Postgres CPU is fully utilized, showing the database is actually saturated instead of bottlenecked on contention.

There are Static code analyzers which already would have detected that.

And these were also automatic. Looks very likely that the team didn’t give a damn about top basic security and good practices.

Like a house made of paper wouldn’t be an example of the insecurity of the construction industry.

> Misconception 1: specification documents are simpler than the corresponding code

Anyone who studied software engineering, should know that specification doesn’t bother with implementation details of the underlying technology.

Things such as quite specific engine are used, are the contents of an encapsulated subsystem.

Proper software engineering specification is incompatible with a hacker culture and picking technology beforehand is a bad practice. It’s much closer to waterfall than to C4.

However, the last 20 years we got software building blocks which impose system architectural restrictions: frameworks. And also pieces of software which are half cooked systems.

Far are the days of requirements, preconditions, postconditions and invariants, network diagrams and entity relationship models.

So in a couple of years we will have de MacBook Neo Neo?

I think they got just cheaper marketing since jobs died. No focus or brand protection.

I often want to try, but never get the time, aren’t you missing packages and solutions out of the shelf and ready to use?

This was AI generated right? And saying that in 2010 Linux was complex and needed to compile everything across virtual machines for cloud solutions and that socket solved that… really in what universe people lived?

Docker made convenient distribute some functionalities which were planned as stack of services rather than packaging appropriately for each distribution and handling to an administrator the configuration. That’s it. And it has many inconveniences. And Linux as well as BSD had containers before and chroots and many other things.

All the issues you mention are about uncertainty.

Uncertainty is one of the largest perceived threats by the human brain, it’s normal you feel it like a threat, it can even cause you anxiety and force you to take severe and unnecessary decisions. If that’s the case talk to a mental health professional because it is not an issue.

However if mental health is not an issue, try some of the many techniques that are there on how to handle uncertainty psychologically, you may start with stoicism (a modern book is fine) and with distribution of risk only of the threats that are an actual problem to you and you have any little of control over them

They will wish that you use an official API, follow the funnel they settled for you, and make purchases no matter how

I get where you come from, but really needs it to be a whole SQLite instance per database? Wouldn’t be more efficient just logic separation in a larger DB?

Better usage of resources and it always allows a parent style agent do complex queries (e.g: intersection of two different actors data doesn’t need to fetch all, copy and do it in buggy non sql code)

Literally the first line of the link:

“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“

My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.

I like a lot of the idea behind such theorem provers, however, I always have issues with them producing compatible code with other languages.

This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.

So no way of leveraging an existing ecosystem.

Are you an AI just summarizing the article?

I think the only people who burnt of the discussion were people who is terminally online. But in the industry, there is people in any paradigm with any previous development times you can remember of.

> Is there any formal language that is usable as general-purpose programming language I don't know of?

That’s sort of my point, the closest thing to a rich type system yet pragmatic enough is to me F# and it’s still falls short as formal verification and ecosystem integration.

I think eventually, we should invest into this direction so LLM production can be trusted, or even ideally, producing or helping with the specific specifications of models. This is yet to be done.

I don’t want to make a prophecy, but the day, ergonomics and verification meet in an LLM automated framework, this new development environment should take over everything previous.

And also with Ada which would be even safer. And the same it is for me... we all got trained in skills are slowly going to fade away.