We remember the Freeman. We are coterminous. For a brief time you joined us. You are one. Between the worlds. Communion of the vortessence. And that other: a deeper mystery. No deeper than the void itself.
I see what you mean, Doktor Leibniz speaking through the centuries, we’re working on it.
Yep, Liebniz was definitely ahead of his time in a lot of aspects of his thought. Or perhaps precisely on time, and the rest of us are still catching up.
Cybernetics seems like a mix of hippie-ish philosophizing and government/military interest in the human use of human beings, to study principles of control that applies to animals and machines. It was an intellectual trend that passed, and there are newer fields, concepts and frameworks.
One of the interesting thing about Cybernetics was just how popular it was, around the late 1970s and early 1980s. I’m talking pop-culture popular. It was referenced in New Wave music and Italian disco (which themselves crossed over much more than you might think, but that’s another story). And it was against this musical backdrop - which was already exploring these ideas - that William Gibson invented Cyberpunk.
We will remember all things
And never know love
And never know how to hate
We will remember all things
And never know love
And simply impersonate
We shall continue with time
And never know why
The reason we came to be
We shall continue our line
And thank you for your gift
Eternity
Thank you Norbert Weiner
Thank you for everything
Thank you Norbert Weiner
Thank you for your believing
1 Like
I think so, yes. “Programming” (instructing a very particular machine to do something) is a very small subset of “modelling” (describing information such that many things can be done to it by many different machines or systems).
We don’t seem to have much in the way of languages for modelling or even data representation. CSV, JSON and XML, I guess? RDF for graphs? SQL for tabular data? A whole bunch of extremely special-purpose data-export formats for individual software packages?
XML plus schemas is already pretty good for data representation, and has been around for long enough that we have decent tooling and lots of experience.
What’s missing is behavior. I’d go for a specification language rather than a programming language. In fact, that’s what I have been pursuing with Leibniz.
3 Likes
I use “modelling” and “specification” interchangeably.
Can someone give me an XML schema that holds two natural numbers X and Y, such that X < Y ?
I also believe that XML is a good starting point due to its universality. But it cannot express all properties.
To check for general predicates, we need to have general programs that do that.
2 Likes
Indeed, you have to choose between general predicates and simpler-than-Turing-complete data models. XML went for the latter, which I think is the right choice for its intended use cases. Other use cases require different trade-offs.
I would like both a declarative way and an operational way to do that. Perhaps they can be bridged by theorem provers.
2 Likes
Then your theorem prover becomes a dependency of your modelling system. Which is fine in some settings but not in others. It’s fine if the audience is familiar with theorem provers (knowing at least what a theorem prover does), and if the overhead of using a theorem prover is acceptable.
The important thing is to check that our implementation is correct at runtime.
That our model correctly reflects the implementation.
If not, then we can have cascading effects, where one piece of the code will corrupt the whole system.
It is necessary to do that to have modularity.
I want to be able to pick a random piece of code from the internet, from unknown sources, and place it in my code / system that contains important and sensitive information and be safe. For this to work, you need to trust that the predicate checks will report any errors.
We need to find errors locally, to also have accountability. Checking the predicates can be done in any language. Agda, a theorem prover, has the ability to both define a specification and at the same time check the predicates at runtime. That is why I prefer it to other modelling languages like (TLA++) or leibniz for example.
1 Like
I want to emphasize the difference between code that is written by experts and code written by users with regards to reusability.
Till now, we use libraries that experts in the specific field have created. If we are to have lithification, or the adaptation of a piece of code by users and not a single common library, and then be able to share it to others, we need to have a way to trust this piece of code. And we can’t do it by trusting the programmer, because he is just a user that has incomplete knowledge of the field.
Thus malleability and lithification demands to find new ways of trusting this piece of code. It is for this reason that I started looking at theorem provers in the first place.
1 Like
It all depends on what you consider evidence for trust. For the kind of code I use, type correctness is very weak evidence. The most common mistakes in my domain are the incorrect transcription of mathematical formulas into code. A missing factor 2, a misplaced minus sign, etc. Type checking is not of much help there. I should be able to read and understand every bit of code I take from others.
This is one reason why I don’t believe in a universal malleable system for everyone. Needs differ in different domains.
3 Likes
