3 ms·
I think it's not just about termination, it's broadly about restricted semantics. If we had a meta-language like Lisp or ML that had very good capabilities to
by nextos 6y ago
I think it's not just about termination, it's broadly about restricted semantics.
If we had a meta-language like Lisp or ML that had very good capabilities to quickly develop DSLs with very clean restricted semantics for every particular component of a big system, and tooling to automate proofs for said restricted semantics, it'd be much easier to prove the validity of any piece of code.
The scenario we currently have is quite different, so it requires heroic efforts to get any kind of guarantee on big systems (e.g. the Astree static analyzer or seL4).
Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy".
- rstuart4133 6y ago> Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy". I posited here on HN Postscript / PDF recently is just such a tar pit, but got down voted for it. If you've every tried to copy and paste from a PDF and got rubbish (as opposed to a message saying you aren't allowed to do that), the reason is the Turning complete program painting the page doesn't have to paint things in a particular order and the things it paints may be bit maps. In the worst case you may as well be trying to copy a bunch of PNG images that have been plonked onto the canvas that happen to look like letters to a human. We would have been far better off with a declarative way of painting a page. It's not that hard - SVG achieves the same end result, and is purely declarative.