4 ms·

I don't have gripes with Rust per se, but I do take issue with the contingent of commenters that seem to not understand the value of a formal specification in t

I don't have gripes with Rust per se, but I do take issue with the contingent of commenters that seem to not understand the value of a formal specification in the construction of formal computational systems in the first place. Basically every computational system lives and dies on its degree of formal specifiability, and having more formal specification is always better unless you are cool with being beholden to the fact that some particular implementation of some program happened to work at some point in time for some input once. That insecure ground is what you're standing on if you don't think formal specifications have any value. In the world of computation, the specification is the system, modulo incidental properties of implementation like performance.

aw1621107 1y ago
> in the construction of formal computational systems > Basically every computational system lives and dies on its degree of formal specifiability How much software development work would you say qualifies as "construction of formal computational systems"? I feel like I have to be thinking of something different than you because to a first approximation I think ~no software has much in the way of formal specification done on it, if any at all. I feel like there's a bit of black-and-white thinking here as well. It's not as if you pick either "full formal specification with bonus Lean/Coq/etc." or "YOLO" - there's shades of grey in between where you can nail down different bits with more or less specificity/formality/etc. depending on feasibility/priorities/etc. Same with support for/against a formal spec - there's more nuance than "an absolute necessity" or "a waste of time".
- voidhorse 1y ago
  > How much software development work would you say qualifies as "construction of formal computational systems"? All of it. That's a literal definition of what a piece of software is, a formal system for computing things. Whether we realize it or like it or not, that's what we are doing when we build software, and that's why formalization of implementation-independent details is almost always beneficial. Sure, you don't always need to do this formalization in Lean or something, but you should at least have a document that outlines the behaviors of the system, it's invariants, etc. etc. Simply pointing people at a codebase and saying "there it is" or making the present, incidental behavior of an implementation the source of truth is like building a bridge and answering the question "how do we know it won't collapse under load X" by answering "idk put the load on it and see". I know it sounds a bit extreme, but I actually would stick to my original stance here. If you have an implementation but haven't worked out its design formally then you probably have a buggy implementation. An aversion and under appreciation of formalism is far more endemic in contemporary software development than a penchant for it is. Arguably, if people in the industry took the title of "engineer" a little more seriously, we'd have better systems. Civil engineers work out formal specifications for bridges even when they are working on a tiny foot bridge in a park, why? because that's basically the whole job. They don't throw their hands in the air and just say "a formal spec ain't worth it, just build the bridge intuitively"—plenty of bridges are built this way, but we don't call those builders engineers, and for good reason. I completely agree that in reality, we often cannot achieve the ideal precisely for the reasons you described. Constraints may make it infeasible. But for the particular case of Rust, I'd argue that that isn't the case, and my point is more so that those entertaining the idea that formal specification doesn't even have value might be doing something with computers, but it isn't engineering.
  - asa400 1y ago
    People build stuff informally all the time, and that stuff very often works fine. Rich Hickey digs into this in some detail. It's not that types or formal methods or rigorous specs or automated tests (or whatever else - pick your formalism) have no value, but they always have a cost as well, and there are many, many existence proofs of systems being built without them. To me, that seems pretty compelling that formalisms in computing should be "a la carte". I think my biggest objection to mandating formalism (in the abstract - I do find value in it in some situations) in computing is how little we know about computing compared to what we know about aviation or bridge building. Those are mature industries; computing is unsettled and changing rapidly. Even the formalisms we do have in computing are comparatively weak.
    - voidhorse 1y ago
      > I think my biggest objection to mandating formalism (in the abstract - I do find value in it in some situations) in computing is how little we know about computing compared to what we know about aviation or bridge building. I don't think that we should mandate formalism. I'm just trying to say that diminishing the value of formalism is bad for the industry as a whole. And point taken about maturity, but in that sense if we don't encourage people to actually engage in defining specification and formalizing their software we won't ever get to the same point of maturity as actual engineering in the first place. We need to encourage people to explore these aspects of the discipline so that we can actually set software on better foundations, not discourage them by going around questioning the inherent value of formalism. Rust is a particularly good example because, as other commenters have pointed out, if we believe it's a waste of time to formalize the language we purportedly want everyone to use to build foundational software, what exactly would we formalize then? If you aren't going to formalize that because it "isn't worth it", well, arguably, nothing is worth formalizing then if the core dependency itself isn't even rigorously defined. People also forget the other benefits of having a formal spec for a language. Yes it enables alternative implementations, but it also enables people to build tons of other things in a verifiably correct way, such as static analysis checks and code generators.
IshKebab 1y ago
> having more formal specification is always better True, all other things being equal. But your logic falls down when all other things aren't equal. Rust is a more "secure ground" than C even though C has an official specification and Rust doesn't really. Also you shouldn't say "formal specification" in this context because I don't think you really mean https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification

aw1621107 1y ago

> in the construction of formal computational systems > Basically every computational system lives and dies on its degree of formal specifiability How much software development work would you say qualifies as "construction of formal computational systems"? I feel like I have to be thinking of something different than you because to a first approximation I think ~no software has much in the way of formal specification done on it, if any at all. I feel like there's a bit of black-and-white thinking here as well. It's not as if you pick either "full formal specification with bonus Lean/Coq/etc." or "YOLO" - there's shades of grey in between where you can nail down different bits with more or less specificity/formality/etc. depending on feasibility/priorities/etc. Same with support for/against a formal spec - there's more nuance than "an absolute necessity" or "a waste of time".

voidhorse 1y ago
> How much software development work would you say qualifies as "construction of formal computational systems"? All of it. That's a literal definition of what a piece of software is, a formal system for computing things. Whether we realize it or like it or not, that's what we are doing when we build software, and that's why formalization of implementation-independent details is almost always beneficial. Sure, you don't always need to do this formalization in Lean or something, but you should at least have a document that outlines the behaviors of the system, it's invariants, etc. etc. Simply pointing people at a codebase and saying "there it is" or making the present, incidental behavior of an implementation the source of truth is like building a bridge and answering the question "how do we know it won't collapse under load X" by answering "idk put the load on it and see". I know it sounds a bit extreme, but I actually would stick to my original stance here. If you have an implementation but haven't worked out its design formally then you probably have a buggy implementation. An aversion and under appreciation of formalism is far more endemic in contemporary software development than a penchant for it is. Arguably, if people in the industry took the title of "engineer" a little more seriously, we'd have better systems. Civil engineers work out formal specifications for bridges even when they are working on a tiny foot bridge in a park, why? because that's basically the whole job. They don't throw their hands in the air and just say "a formal spec ain't worth it, just build the bridge intuitively"—plenty of bridges are built this way, but we don't call those builders engineers, and for good reason. I completely agree that in reality, we often cannot achieve the ideal precisely for the reasons you described. Constraints may make it infeasible. But for the particular case of Rust, I'd argue that that isn't the case, and my point is more so that those entertaining the idea that formal specification doesn't even have value might be doing something with computers, but it isn't engineering.
- asa400 1y ago
  People build stuff informally all the time, and that stuff very often works fine. Rich Hickey digs into this in some detail. It's not that types or formal methods or rigorous specs or automated tests (or whatever else - pick your formalism) have no value, but they always have a cost as well, and there are many, many existence proofs of systems being built without them. To me, that seems pretty compelling that formalisms in computing should be "a la carte". I think my biggest objection to mandating formalism (in the abstract - I do find value in it in some situations) in computing is how little we know about computing compared to what we know about aviation or bridge building. Those are mature industries; computing is unsettled and changing rapidly. Even the formalisms we do have in computing are comparatively weak.
  - voidhorse 1y ago
    > I think my biggest objection to mandating formalism (in the abstract - I do find value in it in some situations) in computing is how little we know about computing compared to what we know about aviation or bridge building. I don't think that we should mandate formalism. I'm just trying to say that diminishing the value of formalism is bad for the industry as a whole. And point taken about maturity, but in that sense if we don't encourage people to actually engage in defining specification and formalizing their software we won't ever get to the same point of maturity as actual engineering in the first place. We need to encourage people to explore these aspects of the discipline so that we can actually set software on better foundations, not discourage them by going around questioning the inherent value of formalism. Rust is a particularly good example because, as other commenters have pointed out, if we believe it's a waste of time to formalize the language we purportedly want everyone to use to build foundational software, what exactly would we formalize then? If you aren't going to formalize that because it "isn't worth it", well, arguably, nothing is worth formalizing then if the core dependency itself isn't even rigorously defined. People also forget the other benefits of having a formal spec for a language. Yes it enables alternative implementations, but it also enables people to build tons of other things in a verifiably correct way, such as static analysis checks and code generators.

IshKebab 1y ago

> having more formal specification is always better True, all other things being equal. But your logic falls down when all other things aren't equal. Rust is a more "secure ground" than C even though C has an official specification and Rust doesn't really. Also you shouldn't say "formal specification" in this context because I don't think you really mean https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification