Hacker News new | ask | show | jobs
by yaccz 1404 days ago
> 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.

2 comments

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.

[0] https://blog.adacore.com/recordflux-from-message-specificati...

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)