|
|
|
|
|
|
by littlestymaar
1130 days ago
|
|
|
> Also, as I said on this item [2], Rust is no panacea. […], but if your programming language does not have a semantics you cannot even begin to ask if your code is correct because the question itself doesn't make any sense. AFAIK safe Rust is OK, but that's true that unsafe Rust has been pretty much “whatever LLVM will do with the IR that rustc generates”, but properly formalizing the semantic has been ongoing for years and has already started to give actionable results. The current state of things is still far from optimal, but at the same time you're always going to have an implementation of your programming language before you have a formal semantic, because nobody is ever going to use a language with a semantic but no implementation… |
|
|
I appreciate what you're saying, however, hear me out. Suppose we had a language with a defined semantics and a useable implementation. We could use that language to implement, say Rust, and in so doing have a semantics for Rust, a semantics defined by its implementation. The point is, to be principled, we have to start somewhere. Make that language basic so that we are capable of providing a semantics. Now, granted, the "semantics" we generate for Rust in doing so will be necessarily pessimistic, i.e. overly determined. But then one could develop tooling to "prune" the implementation defined semantics somehow towards an idealized semantics. I don't think anyone has seriously pursued this avenue of thought.
Also, I must add, I appreciate your thoughtful elision from my quote. I need to stop getting worked up. But truly, software feels like it's perpetually in the dark ages. We have such incredible compute power thanks to the tireless effort of hardware engineers, and still we're programming with the equivalent of "stone knives and bear skins".