5 ms·

How this improvement translate into real world agentic coding task ?

• ogogmad 10mo 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 10mo ago
    It would be helpful in automating the busy work of many verification aware programming languages. At least the Dafny authors are excited about it.
    • nextos 10mo ago
      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.
    • naasking 10mo ago
      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.
  • simulator5g 10mo ago
    This already exists: https://www.wolframalpha.com/ https://www.wolframalpha.com/
    • ogogmad 10mo ago
      Since you're bad at maths, you think being good at maths is being a calculator like WolframAlpha.