3 ms·
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.
by ogogmad 11mo ago
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.
- indolering 11mo agoIt would be helpful in automating the busy work of many verification aware programming languages. At least the Dafny authors are excited about it.
- nextos 11mo agoIMHO, 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.
- naasking 11mo agoAnother 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.
- simulator5g 11mo agoThis already exists: https://www.wolframalpha.com/ https://www.wolframalpha.com/
- ogogmad 11mo agoSince you're bad at maths, you think being good at maths is being a calculator like WolframAlpha.