Theorem Provers Are Refactoring Tools

แชร์
ฝัง
  • เผยแพร่เมื่อ 18 ธ.ค. 2024

ความคิดเห็น • 11

  • @JamesPaulWhite
    @JamesPaulWhite 3 หลายเดือนก่อน

    Excellent!

  • @RodolfoHansen
    @RodolfoHansen 3 หลายเดือนก่อน

    I love how you stumbled upon this... It makes total sense given the normalization / reduction steps taking place...

    • @craftvscruft8060
      @craftvscruft8060  3 หลายเดือนก่อน +1

      Absolutely, it's one of those moments when you realize you've learned the same concept twice for different reasons, it opens up possibilities.
      I think compiler passes are another example of this concept, semantics-preserving tree transformations. So some of the work on certified compilers should be applicable to refactoring

  • @Maedas
    @Maedas 3 หลายเดือนก่อน

    I found this interesting, but am a little disappointed that the issue of choosing what rules to apply during the refactoring ended up being solved by using an existing library without (me) understanding the underlying process fully.
    You kind of gloss over your own knowledge there, I have no idea how you confidently defined the list of manual refactoring steps (14:23) and would love to see a video about it from your POV, be it methodology or just raw experience.
    Regardless, I'm glad I stumbled across your video and hope to see more of your videos in the future :)

    • @craftvscruft8060
      @craftvscruft8060  3 หลายเดือนก่อน +1

      Thanks @Maedas, this is very helpful feedback! I've been making some more advanced content this year and I'm not always very good abount saying what knowledge it depends on. I'll try and improve that going forward.
      I'm linking my playlist of refactoring videos and the older ones are more focused on my thought process as it occurs rather than these new techniques for tool support.
      Better yet, some teacher's that I look up to on this are Arlo Beshee (e.g. "Mastering Legacy Code Incrementally" talk) and Emily Bache (channel @EmilyBache-tech-coach). Cheers!
      th-cam.com/play/PLRe4i06eNAcDY4XjMfyEMK6hjnoIOpqk2.html

    • @craftvscruft8060
      @craftvscruft8060  3 หลายเดือนก่อน +1

      Oh, and the specific list of rules you're asking about were the same ones that I wrote in the Comby UI while inspecting the code in 9:45 - 13:00, if that helps at all.
      Mostly Boolean Logic simplification - might be a good topic for a followup video.

    • @Maedas
      @Maedas 3 หลายเดือนก่อน

      @@craftvscruft8060 Yeah the list is no problem, I saw and understood what you did I just have no idea how you came to the choices you did while doing it; If I had to build something like that it would take me 30 min and I would be very unsure about my methodology, kind of just guessing/looking at articles/asking around.
      A follow up on Boolean Logic simplification sounds lovely

    • @Maedas
      @Maedas 3 หลายเดือนก่อน

      @@craftvscruft8060 thank you for taking my feedback correctly, I don't mean to be negative and am just straightforward in general 😅
      Thank you, I'll check the playlist and the names out

  • @steveasher
    @steveasher 3 หลายเดือนก่อน

    Wow! What if Ray solves refactoring? If teams could run an auto-refactoring tool that executes a bunch of reasonable refactoring rules in the same way they currently run their auto-formatting tool, it sort of changes everything.

    • @craftvscruft8060
      @craftvscruft8060  3 หลายเดือนก่อน +1

      Ray-Factor does have a ring to it :) I see refactoring as something where the target depends on your current goals, so I don't know if it'll ever be quite as fire-and-forget as formatting/linting. But these kinds of workflows - express one intention and 30 steps unfold - I think that's very possible.
      A major limiting factor is that our mainstream languages are not verification-friendly, so we either climb that analysis mountain or write more code in provable languages. Purely-functional languages might have a new secret weapon.