> the text is just a tool to manipulate some abstract model of the program.
yup.
> When you think about it this way, it becomes clear that using a textual source code is really inefficient way to manipulate this model.
Hard nope. All the attempts at different approach were a failure so far. Text so far is the best thing we have because text can be analyzed formally and computed with by computers. This is the result of the work that's being going for at least like 200 years in philosophy, logic, and math.
What we really need is to bridge the gap between programming and math as industry standard, not academical exersise somehow. But I highly doubt eliminating text as source code is it.
To add to this, I think text still needs to be the canonical representation of programs. But we're still ways away with tools to express ways we want to modify, generate code. I think the late Pieter Hintjens had the right of it: we should generate code more often (I know it's polemic here). Not behind some magic curtains like the overly complex (for me) and difficult-to-inspect c++ templates but actual code generators.
One example: recordflux [0] generates, from a high-level dsl, SPARK code that can be proved to be Absent of Run-Time Error. It has a model checker for high-level constraints but lays out serialisation/deserialisation code to access fields. They've been recently working protocol/session-level modeling and it's getting very interesting.
I have a similar tool that I use to generate AORTE serdes code, but once you have that, you can go on to generate fuzzers, proxies to other techs.
We're probably also missing a way to target interesting intermediate representations of programs (either Why3 VCs, cbmc GOTO, but maybe also to lean 4 or whatever temporal logic tool of the day, or other automated/assisted proof or generation environments).
Writing those is a huge undertaking every time, and a lot of duplicated
potentially buggy effort. I look at the amazing work that's been done (and still being done) to bring up libadalang, a parsing and high level semantic query tool that changed my day-to-day coding paradigm. One of the missing pieces of the puzzle is to me the 'generic
parser and semantic specification' that would generate an interpretor and all those proxies for you.
To be clear, I don't think we should get rid of text completely, or use some drag&drop UI or some visual model. It's just the program should be defined by the semantic model first and then viewed/edited however it is practical (often by text again).
And we already do this in many places - many common code changes we do are already automated by IDE (which maintains the model in memory), so we don't edit the text directly and we don't even think about it that way, we think about how we want to transform the model (ie. extract a function), not about how the text moves between files.
> Text so far is the best thing we have because text can be analyzed formally and computed with by computers.
This doesn't make too much sense to me. Using the approach I talk about would actually make that much easier, because tools wouldn't need to parse the text and work directly on the semantic representation (i.e. it's much easier to query a database than extract the information from textual sources)
> The historic reality is that HTML served as a "backdoor"/gateway to let the linux community compete with microsoft: linux devs could ship their code for windows clients.
Problem is you need to remember the patterns first to be able to think "hey I know this pattern. Maybe if I look up what the identity is it will be usefull"
The claim is only missing a qualification that the impossibility exists within the framework of ieee 754. It can be easily inferred from context and it is important to note because thats what the major CPU architectures use to store native floating point numbers. Therefore, the point is, we need a non-native (wrt the cpu) way to store and calculate with irrationals and some rationals if mathematical precision is required.
> If something is being described that is hard to do, then the sentence is structured in such a way that it is comparatively hard to understand, by using an unusual word order etc. If things are far apart, the words are themselves far apart etc. For quick things, words are omitted that cannot be omitted in other languages etc.
