4 ms·

What's a formal language?

• ngruhn 1y ago
  You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper proofs that people normally produce. Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm: shortestPath(graph, start, end) You could proof something like: For all `graph` and each `path` in `graph` from `start` to `end`: path.length <= shortestPath(graph, start, end).length
• Someone 1y ago
  The only definition I know of is https://en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Formal_language. I also think that is the commonly accepted definition. Taking that as the definition, this definitely is not the first formal language learnable in 1-2 hours. I would think, for example, that the language consisting of just the empty string is older and learnable in 1-2 hours. They probably mean something like “formal language used for writing mathematical proofs that is (about) as powerful as Lean”, though.