3 ms·
> The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started. I believe this to b
by User23 4y ago
> The largest barrier to greater adoption of languages like Coq with proof systems built-in is the formal background needed to get started.
I believe this to be a language problem and not a conceptual problem. All that you need to pragmatically formalize semantics is Hoare triples and basic predicate calculus[1]. Anyone that can understand an if statement already has the necessary conceptual machinery. The so-called “formal methods” community delights in over complicating the problem with gadgets like category theory. Which is ironic, because they’re introducing the same kind of unnecessary complexity that causes the problem that they’re trying to solve.
[1] ok that’s not utterly strictly true because arrays (or mutable functions, as I like to think of them) present some subtleties, but those are more a problem for the definers rather than the users.
- thaliaarchi 4y agoI was referring to how the communities of these languages typically frame the problem, so you need formal background to read the materials published on it. As you say, this is a major barrier. This is where Rust shines, in that they've framed the language in terms of how its used, developed accessible documentation, and steered away from delving into the theory behind it.