3 ms·
> 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 comp
by 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.