Skip to main content

Questions tagged [formal-languages]

A formal language is a collection of words over an alphabet, i.e. strings of symbols from the alphabet, according to certain rules. (from nLab)

Filter by
Sorted by
Tagged with
19 votes
3 answers
7k views

Can the language of proof assistants be used for general purpose programming?

Planning on learning lean/lean4, I was wondering if a proof assistant system like lean4 can be used for general purpose programming? For example, can it replace a language like Standard ML? More ...
tinlyx's user avatar
  • 2,034
1 vote
1 answer
145 views

Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
HighAsAKiteOnMath's user avatar