IMHO, this remains a great space to explore. You type some formal specification in e.g. Hoare logic, and a mix of SAT/SMT and LLMs autocomplete it. Correct by definition.
It would also facilitate keeping engineers in the loop, who would decompose the problem into an appropriate set of formally specified functions.
They could also chip in when necessary to complete difficult proofs or redefine the functions.
Another possibility is to automatically annotate a software with assertions, preconditions, postconditions or other verification annotations based on the languages semantics and programmer intent, and then run a verifier on the result and evolve the program and annotations based on that intent. So for C, it could fill in data needed by Frama-C.
It doesn't. However, having a free-of-charge maths genius available 24/7 has broad potential. It's hard to predict what it will be used for.
This already exists: https://www.wolframalpha.com/
Since you're bad at maths, you think being good at maths is being a calculator like WolframAlpha.
It would be helpful in automating the busy work of many verification aware programming languages. At least the Dafny authors are excited about it.
IMHO, this remains a great space to explore. You type some formal specification in e.g. Hoare logic, and a mix of SAT/SMT and LLMs autocomplete it. Correct by definition.
It would also facilitate keeping engineers in the loop, who would decompose the problem into an appropriate set of formally specified functions.
They could also chip in when necessary to complete difficult proofs or redefine the functions.
Another possibility is to automatically annotate a software with assertions, preconditions, postconditions or other verification annotations based on the languages semantics and programmer intent, and then run a verifier on the result and evolve the program and annotations based on that intent. So for C, it could fill in data needed by Frama-C.