Craft vs Cruft
Craft vs Cruft
  • 74
  • 53 389
Reinventing Boolean Algebra (Lean Prover)
Craft vs Cruft: Meditations on software quality. Episode 57: Reinventing Boolean Algebra (Lean Prover)
References:
Previous video: Theorem Provers are Refactoring Tools
ua-cam.com/video/UdB3XBf219Y/v-deo.html
Boolean Algebra course videos
ua-cam.com/play/PLTd6ceoshprcTJdg5AI6i2D2gZR5r8_Aw.html
Lean prover
lean-lang.org/
Boolean Algebra Simplifier
www.boolean-algebra.com
Follow Ray Myers:
LinkedIn: www.linkedin.com/in/cadrlife
Twitter: lambdapocalypse
Empathy In Tech podcast: empathyintech.com
Mender.AI
Переглядів: 281

Відео

Theorem Provers Are Refactoring Tools
Переглядів 2632 місяці тому
Craft vs Cruft: Meditations on software quality. Episode 56: Theorem Provers Are Refactoring Tools Follow Ray Myers: LinkedIn: www.linkedin.com/in/cadrlife Twitter: lambdapocalypse Empathy In Tech podcast: empathyintech.com Mender.AI References: Source code: github.com/raymyers/verified-refactoring Gilded Rose kata, Emily Bache Repo github.com/emilybache/GildedRose-Refactoring-Kata ...
Core Conflicts In Reliability: Having Our Cake and Eating It
Переглядів 942 місяці тому
Craft vs Cruft: Meditations on software quality. Episode 55: Core Conflicts In Reliability: Having Our Cake and Eating It References: Beyond The Goal by Eli Goldratt www.audible.com/pd/Beyond-the-Goal-Audiobook/B002V1LYO2 Steve Tendon and TameFlow tameflow.com Karl Perry and The Conflict Club yourthinkingcoach.com It's Not Luck by Eli Goldratt www.amazon.com/Its-Not-Luck-Eliyahu-Goldratt/dp/088...
Automated Gilded Rose Refactor
Переглядів 1783 місяці тому
Craft vs Cruft: Meditations on software quality. Episode 54: Automated Gilded Rose Refactor Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse Empathy In Tech podcast with Andrea Goulet empathyintech.com References: Verified Refactoring repo github.com/raymyers/verified-refactoring Gilded Rose kata collection github.com/emilybache/...
Gilded Rose with Provable Rewrites in C (Symbolic Execution)
Переглядів 2615 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 53: Gilded Rose with Provable Rewrites in C (Symbolic Execution) Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse References: Repo github.com/raymyers/gilded-rose-c-symbolic-execution Gilded Rose kata collection github.com/emilybache/GildedRose-Refactoring-Kata Klee klee-se...
Goal Tree | Craft vs Cruft 52
Переглядів 1646 місяців тому
Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse References: Previous episodes on Theory of Constraints ua-cam.com/play/PLRe4i06eNAcA6s2w9YhSz_8TCsqG_G1eU.html Goal Tree video by Bill Dettmer ua-cam.com/video/6ClpgEzJxFE/v-deo.html Logical Thinking Process (Marris Consulting course page) logicalthinkingprocess.podia.com
NEW PODCAST
Переглядів 976 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 51: NEW PODCAST Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse Follow Andrea Goulet www.linkedin.com/in/andreamgoulet empathyintech.com Upcoming Conferences: Mendercon 2024 mendercon.com Artificially Intelligent Enterprise www.techstrongevents.com/the-artificially-intelli...
Substance of Success w/ Dylan Evans | Craft vs Cruft 50
Переглядів 636 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 50: Substance of Success Follow Dylan Evans: Simple Salt: simple-salt.com LinkedIn: www.linkedin.com/in/dylanevans-makesecuritysimple/ Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse
Dissecting Devin | Craft vs Cruft 49
Переглядів 3217 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 49: Dissecting Devin Nopilot Article: Dissecting Devin nopilot.dev/blog/dissecting-devin Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Nopilot.dev Mender.AI Twitter: lambdapocalypse References: Previous Episode: Devin Has Been Beaten ua-cam.com/video/pc55pfHpigs/v-deo.html Previous Episode: Will AI Democratize Progra...
Devin Has Been Beaten
Переглядів 2,7 тис.7 місяців тому
New site: nopilot.dev Current presumptive leader, AutoCodeRover by Automated Program Repair @ NUS: github.com/nus-apr/auto-code-rover Previous Episode: "We Can Beat Devin" ua-cam.com/video/IM5oi2ycNIY/v-deo.html Follow me on LinkedIn: www.linkedin.com/in/cadrlife
Decoding Democracy w/ Lucia Bourgeois | Craft vs Cruft 48
Переглядів 987 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 48: Decoding Democracy Follow Lucia Bourgeois www.linkedin.com/in/lucia-bourgeois/ Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Mender.AI Twitter: lambdapocalypse References: Missouri Startup Weekend www.mosw.io/ Previous Episode "Conflicts Don't Exist (The Evaporating Cloud)" ua-cam.com/video/wP1vD2pguvs/v-deo.html...
Conflict Clouds as Personal Growth w/ Karl Perry | Craft vs Cruft 47
Переглядів 1097 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 47: Conflict Clouds as Personal Growth Follow Karl Perry and "The Conflict Club" yourthinkingcoach.com LinkedIn: www.linkedin.com/in/karlgperry/ Follow Ray Myers LinkedIn: www.linkedin.com/in/cadrlife Mender.AI Twitter: lambdapocalypse References: Previous Episode "Conflicts Don't Exist (The Evaporating Cloud)" ua-cam.com/vide...
We Can Beat Devin | Craft vs Cruft 46
Переглядів 4097 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 46: We Can Beat Devin Follow me on LinkedIn: www.linkedin.com/in/cadrlife Mender.AI Twitter: lambdapocalypse References: Cognition Labs Devin announcement www.cognition-labs.com/introducing-devin Past video "Will AI Democratize Programming" ua-cam.com/video/7YxD8R9Q_Bo/v-deo.html Channel: @CanWeBeatDevin Discord: discord.gg/ky...
ChatBot (STILL) Claims To Be Licensed Physician (Dr Gupta AI)
Переглядів 907 місяців тому
Views expressed are my own and do not represent my employer. Past episode: "Dr Gupta AI: ChatBot Claims To Be Licensed Physician" ua-cam.com/video/2RTkkEKFyEk/v-deo.htmlsi=OHCwwzarKmP3qKRo Past episode: Aspiring Luddite ua-cam.com/video/WugbbKdgv5Y/v-deo.htmlsi=nNFYNDGt8RAIFJmq Credit to Arthur Etchells for finding this issue. asketch/status/1649524842599796736 Follow me on LinkedIn...
Provable Linked Lists - Part 2 Dafny | Craft vs Cruft 45
Переглядів 828 місяців тому
Craft vs Cruft: Meditations on software quality. Episode 45: Provable Linked Lists - Part 2 (Dafny) Follow me on LinkedIn: www.linkedin.com/in/cadrlife Mender.AI Twitter: lambdapocalypse References: Dafny Language dafny.org Purely functional datastructures Wiki: en.wikipedia.org/wiki/Purely_functional_data_structure Okasaki book: www.goodreads.com/en/book/show/594288 Key Project, Ja...
Provable Linked Lists - Part 1 Dafny | Craft vs Cruft 44
Переглядів 1868 місяців тому
Provable Linked Lists - Part 1 Dafny | Craft vs Cruft 44
English To Theorems (Z3 + GPT-4) | Craft vs Cruft 43
Переглядів 1608 місяців тому
English To Theorems (Z3 GPT-4) | Craft vs Cruft 43
Semi-Formal Methods | Craft vs Cruft 42
Переглядів 1018 місяців тому
Semi-Formal Methods | Craft vs Cruft 42
AI Accountability Shield | Craft vs Cruft 41
Переглядів 759 місяців тому
AI Accountability Shield | Craft vs Cruft 41
My Stack Runneth Over! w/ Ana Hevesi
Переглядів 1859 місяців тому
My Stack Runneth Over! w/ Ana Hevesi
Aspiring Luddite | Craft vs Cruft 39
Переглядів 589 місяців тому
Aspiring Luddite | Craft vs Cruft 39
RefactorGPT (LabLab.ai Hackathon Entry)
Переглядів 869 місяців тому
RefactorGPT (LabLab.ai Hackathon Entry)
First Order Logic | Craft vs Cruft 38
Переглядів 829 місяців тому
First Order Logic | Craft vs Cruft 38
Layoff Dodging 101 | Craft vs Cruft 37
Переглядів 1,1 тис.10 місяців тому
Layoff Dodging 101 | Craft vs Cruft 37
Refactoring With Proofs | Craft vs Cruft 36
Переглядів 76510 місяців тому
Refactoring With Proofs | Craft vs Cruft 36
Metrics: Naughty or Nice? | Craft vs Cruft 35
Переглядів 5510 місяців тому
Metrics: Naughty or Nice? | Craft vs Cruft 35
Coding a DSL for Theory of Constraints diagrams (TOC-Lang)
Переглядів 14410 місяців тому
Coding a DSL for Theory of Constraints diagrams (TOC-Lang)
Code With No Hands You Cowards! | Craft vs Cruft 34
Переглядів 9111 місяців тому
Code With No Hands You Cowards! | Craft vs Cruft 34
Let's Fire AGI | Craft vs Cruft 33 #FireAGI
Переглядів 278Рік тому
Let's Fire AGI | Craft vs Cruft 33 #FireAGI
Custom GPT Preview: “The Most Tangled Cord”
Переглядів 21Рік тому
Custom GPT Preview: “The Most Tangled Cord”

КОМЕНТАРІ

  • @woosix7735
    @woosix7735 18 днів тому

    wow that's a pretty non constructive intro!

  • @woosix7735
    @woosix7735 19 днів тому

    2024 - the year of formal methods. I like the sound of that

  • @Username-d2v6y
    @Username-d2v6y Місяць тому

    how do i get that ubuntu terminal in windows like the one you are using

    • @craftvscruft8060
      @craftvscruft8060 Місяць тому

      Oh, I think at the time I was using WSL (Windows Subsystem for Linux) w/ Windows Terminal. Nowadays I use OSX with iTerm2.

  • @letscodeitup
    @letscodeitup Місяць тому

    Loved your video and I’d love to check out Acl2. If you’re into rewriting tools, there’s an interesting language called Maude that’s based on rewriting logic that has a lot of tools to make confluent reductions easier from the start. There’s a Church-Rosser checker, which I haven’t tried yet. I’m looking forward to your next video!

  • @Maedas
    @Maedas Місяць тому

    I don't think I have ever felt someone deserved my subscription and more exposure to the algorithm, thank you so much for making this! I'm looking forward to digging deep into this video tomorrow as I just laid down to sleep, and will return the generosity you have provided with feedback after I have digested it properly. Initial thoughts: The introduction daunts me but as soon as you got into coding I noticed I could follow. Appericiate the dark mode for this session and can see what you mean, while readability isn't bad it isn't emphatically good either. Name pronounciation was very acceptable, if you'd ask what I like the most are the "midas" and "made as" variant, without any hard emphasis on any vowel. Lastly, I am from a Sweden and it is 4:47 am right now, was on call this evening. Good night and thanks again!

  • @RudigerWolf
    @RudigerWolf 2 місяці тому

    Great examples of Conflict clouds. Loved video. Thanks for making and sharing.

  • @Maedas
    @Maedas 2 місяці тому

    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 2 місяці тому

      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! ua-cam.com/play/PLRe4i06eNAcDY4XjMfyEMK6hjnoIOpqk2.html

    • @craftvscruft8060
      @craftvscruft8060 2 місяці тому

      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 2 місяці тому

      @@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 <3 I have basically a year and a half into a bachelors degree in Comp Sci but am sadly a bit averse to complex terminology; I feel a lot of jargon is thrown around unnecessarily so I tend to only learn it when I have a legitimate reason to. Given that, I do think that there is a niche on UA-cam of intermediate/advanced videos with simple terminology that really needs more creators, and this video at least was spot on there so highly enjoyable.

    • @Maedas
      @Maedas 2 місяці тому

      @@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 <3 An ending feedback also would be that the sceenshare is a bit bright; it's not something that will hinder me watching but is at the upper end of what my eyes tolerate, so I wonder if it would be possible to make it more... appealing? to dark mode users. I hope you understand what I mean and again it's very optional, but might be beneficial. Hope you have a good day :)

  • @steveasher
    @steveasher 2 місяці тому

    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 2 місяці тому

      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.

  • @JamesPaulWhite
    @JamesPaulWhite 2 місяці тому

    Excellent!

  • @RodolfoHansen
    @RodolfoHansen 2 місяці тому

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

    • @craftvscruft8060
      @craftvscruft8060 2 місяці тому

      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

  • @emilybache
    @emilybache 3 місяці тому

    very cool that you can automate your own refactorings!

    • @craftvscruft8060
      @craftvscruft8060 3 місяці тому

      Great to hear from you, Emily. I think TripService kata is next! For everyone else, her channel is a great source of more refactoring content. www.youtube.com/@EmilyBache-tech-coach

  • @NitsanAvni
    @NitsanAvni 3 місяці тому

    17:53 Another use case is allowing an AI agent to transform code only via automated refactorings.

    • @craftvscruft8060
      @craftvscruft8060 3 місяці тому

      Yep! As we've discussed that's part of what started me down this path. I'm still not sure what the overall workflow looks like but it seems like promising area for LLMs + Tools. mender.ai/blog/turbo-refactoring

  • @NitsanAvni
    @NitsanAvni 3 місяці тому

    Yes! Inspiring. My mind is going in directions!

  • @MikeFinney
    @MikeFinney 3 місяці тому

    “..some really amazing things are going to be possible.” 👏😊 18:23 Workflows ❤

  • @donovan543
    @donovan543 5 місяців тому

    Promo`SM

  • @steveasher
    @steveasher 6 місяців тому

    Another interesting comparison to OKRs is Stephen Bungay's application of modern mission command to business management, as he describes in his book, The Art of Action. Goal Trees, Mission Command, and the, albeit elusive, effective implementation of OKRs all have a lot in common. One interesting thing about mission command, as Bungay describes it, is that it is explicitly intended to decentralize decision making to the people with the most situational awareness, because modern militaries realized a long time ago that centralized decision-making authority and rigid plans of execution do not scale. This decentralized decision making is another important aspect that isn't explicitly enforced in OKRs, and the reality is that the prevailing business culture isn't ready to trust "subordinates" to make decisions -- even within the scope of that employees responsibility, and even if it doesn't scale.

  • @jeremycunningham8494
    @jeremycunningham8494 6 місяців тому

    I still remember the first time, many years ago, I first came across CorgiBytes that I also had the reaction of, “I’m not the only one that likes fixing stuff!” The green field development mindset was so prevalent in the groups I was part of at the time.

    • @craftvscruft8060
      @craftvscruft8060 6 місяців тому

      Absolutely, I felt the same way. People like them and Arlo Belshee, Marianne Bellotti, Chelsea Troy for instance not only showed me skills, they helped me understand my identity. Such a powerful thing.

  • @StonedApe420
    @StonedApe420 6 місяців тому

    My Mind is Blown.

  • @craftvscruft8060
    @craftvscruft8060 7 місяців тому

    Update: Cognition has admitted the point about the incomplete Upwork task, I've updated the Nopilot blog entry with their remarks: nopilot.dev/blog/dissecting-devin

  • @gabrielarmasaranibar9342
    @gabrielarmasaranibar9342 7 місяців тому

    Great video, keet it up!

  • @ekomukanga893
    @ekomukanga893 7 місяців тому

    I just discovered your channel. This is cool!

  • @belooga-bj3pw
    @belooga-bj3pw 7 місяців тому

    It would be great if it were possible to utilize a local llm instead of chatgpt api. I'm restricted by nda right now, so I can't really work with a lot of code without it running locally :(

    • @craftvscruft8060
      @craftvscruft8060 7 місяців тому

      That's a really common issue, and nopilot.dev will also follow the local model use case. For now, I find the r/LocalLLaMA subreddit very helpful for that type of model news. The coding models are becoming usable - especially on machines that can run the bigger ones

    • @hypergraphic
      @hypergraphic 7 місяців тому

      I'm using ollama locally and privategpt looks promising too!

    • @belooga-bj3pw
      @belooga-bj3pw 7 місяців тому

      @@hypergraphic I'm using anythingLLM, it's has an amazing rag

    • @craftvscruft8060
      @craftvscruft8060 7 місяців тому

      @@hypergraphic Great to hear, I'll be writing about the setups people are using, let me know if you find a particular local model is working well

  • @craftvscruft8060
    @craftvscruft8060 7 місяців тому

    New episode on conflict clouds for personal growth out now with Karl Perry! ua-cam.com/video/fBM1E-5Nabg/v-deo.html

  • @jarinboyer
    @jarinboyer 7 місяців тому

    Why don't you just ask it some medical questions both basic and advanced and then fact check the responses instead of repeatedly asking the same nonmedical questions over and over expecting a different result lol

    • @craftvscruft8060
      @craftvscruft8060 7 місяців тому

      Thanks for watching, Jarin! I don't evaluate tools in their capacity to give medical advice because I'm not a qualified medical researcher. This channel is about Software Engineering, my area of expertise. Peer reviewed studies are being done on LLMs in medicine, though I'm not aware of any formal evaluation of this product. The reason I would expect a different result a year later is that the company was made aware of the bug so it would be common practice to fix it. I was also reminded of this case due to a legal dispute involving an airline denying responsibility for what their support chatbot told a customer, covered in my episode "AI Accountability Shield" last month. ua-cam.com/video/HYdzHP1eaCs/v-deo.html

    • @jarinboyer
      @jarinboyer 7 місяців тому

      @@craftvscruft8060 oh that's cool, I didn't know that was the case. I quickly browsed through your channel and you should make some software or a website strictly using chatgpt only with some simple and complex functions included. Id watch that.

    • @cupcakebrown9836
      @cupcakebrown9836 19 днів тому

      @craftvscruft8060, that's a misguided perspective. Instead of limiting the tool to basic functions, consider using it for its intended purpose. It's like using a TI-84 calculator solely for addition and then claiming it's not worth the price because you aren't taking advantage of its advanced features.

  • @craftvscruft8060
    @craftvscruft8060 8 місяців тому

    This still reproduces today: ua-cam.com/video/kOxpn_m3wIY/v-deo.html

  • @steveasher
    @steveasher 8 місяців тому

    Is there a way of classifying how thoroughly code has been proven?

  • @steveasher
    @steveasher 8 місяців тому

    Nice! I'd be interested in seeing a usage example that is directly applicable to some "real world" use case. The first one that comes to mind from my own career is promotional pricing systems. When working for a major retailer I encountered an overly-complicated pricing system that could have been expressed quite succinctly in predicate logic. The obvious challenge with that approach would be in creating a UX workflow that would allow (non-logician) product managers the ability to manage rules in the system. A workflow like the one you show in this video might be the solution to that UX challenge.

    • @craftvscruft8060
      @craftvscruft8060 8 місяців тому

      Thanks, Steve! Yes I think there is a powerful pattern here for as an LLM bridge to DSLs that are readable by domain experts but hard for them to precisely write. DSLs are still notoriously hard to get right but I think this could help them along if we don't forgo the quality of the abstraction

  • @NitsanAvni
    @NitsanAvni 9 місяців тому

    "If you don't do a good job, you're going to be left behind."

  • @steveasher
    @steveasher 9 місяців тому

    I started this video yesterday when I only had a few minutes free to watch it. I'm so glad that I came back to it today! This conversation with you and Ana has given me a lot to think about. Her perspective is immediately applicable to my current role in motivating nonprofit volunteers and computer science students.

    • @craftvscruft8060
      @craftvscruft8060 9 місяців тому

      Awesome! I was also surprised at how relevant some of her points were to daily dev life

  • @arefin-huq
    @arefin-huq 9 місяців тому

    Excited to see this!

  • @NitsanAvni
    @NitsanAvni 9 місяців тому

    Beautiful work! I love the focus on *suggestions*, and the way you leverage capabilities of humans, AIs and traditional software tools.

  • @arefin-huq
    @arefin-huq 9 місяців тому

    Thanks for the introduction to Z3!

  • @steveasher
    @steveasher 10 місяців тому

    Nice! I'm loving the Formal Methods series!

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Thanks, Steve! I see some surprising parallels between formal methods and concept of DSLs you introduced me too way back when. I'll need to think of how to describe it but something to do with getting leverage out of clearly modeling a problem.

  • @leighnorman2579
    @leighnorman2579 10 місяців тому

    💕 *promosm*

  • @apple1231230
    @apple1231230 10 місяців тому

    Layoffs are to be expected at most companies evwntually and something everyone should plan for and hope to never experience. No matter what they say, almost no large corporation actually cares about their employees more than milking every dollar they can. They’ll actively hire more than they need in boom cycles knowing full well they’ll have to make large cuts soon down the line, but they’ll make more money if they hire now and fire later than if they have the appropriate staff. No one is safe, so plan accordingly. If I got fired I’d be more annoyed at having to interview than anything else and secondly annoyed at the lost income for however long it took to find a new job. Having half a year of income saved (I have way more) makes a layoff annoying as opposed to devastating. Forgive me for not caring when someone who makes a lot of money and blows it all due to life style inflation finds themseleves between a rock and a hard spot when they’re laid off out of no where.

    • @apple1231230
      @apple1231230 10 місяців тому

      Also your point of this being a leadership problem is 100% accurate and pertains not only to corporate America but to all societal structures including governance. Power structures across the board result in similar actions and is exactly why giving government more more more of everything does nothing generally except for exasperated preexisting problems. This is not a corporation phenomenon, it is a human psychological power dynamics phenomenon and will almost certainly be with us as a species in perpetuity

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Thanks for the thoughtful response, apple number, I have a couple reactions. Wholeheartedly agree with "No one is safe, so plan accordingly" - that's probably my central message here as well. "Forgive me for not caring when someone who makes a lot of money [...] finds themselves between a rock and a hard spot" Maybe I've misunderstood but I feel like you might be casting casual judgement on an extremely large and varied group if you're implying no one in entire tech sector (or even beyond) would deserve sympathy upon being laid off. We're talking about hundreds of thousands of people and we can't make blanket assumptions about the options they had to do better. Of course we're not too worried about the L6 teamleads but that's beside the point.

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      @@apple1231230 "This is not a corporation phenomenon, it is a human psychological power dynamics phenomenon" I agree with this except where it might imply we can't improve. If we have a natural tendency to organize in power structures and then mistreat eachother that makes it all the more important learn how to temper the impact, like we would do with any other force universal even gravity. That's the philosophical argument and the empirical one is that for almost any kind of worker mistreatment we could find an example of a well-performing company that chooses to do it less. In the case of layoffs Toyota has maintained none for full-time employees for 80 years, right?

    • @apple1231230
      @apple1231230 10 місяців тому

      @@craftvscruft8060 I agree with you saying not to make blanket statements, and everyone has their own unique scenarios. I'm specifically refering to people who for all intents and purposes, (own a house at a good rate, make high salaries, no familial trauma and/or expensive medical needs they're having to deal with, decent mental state, and generally well off etc) are well off but still find themselves in a terrible spot upon being layed off, which is a lot of people. you can make excuses to varying degrees of validity for every problem in ones life, but at the end of the day many people would find themselves in a major pickle if laid off unexpectedly shearly for being terrible with personal finance. i don't feel bad for these people, which i would argue is probably the majority in this situation, assuming were talking corporate lay offs, not factory workers at amazon. as for your second reply i wholeheartedly agree. Im actually a closeted optimist. I think companies should and can do better, but realistically many don't, so one should plan for the worst and look for the best. If you ever find yourself privleged enough to own a company, as i hope to in the future, strive to make it a fair and valuable place to work. My philosophy will be radical transparency. We'll see how that goes.

  • @thecomrade9284
    @thecomrade9284 10 місяців тому

    I like you.

  • @ShotgunAFlyboy
    @ShotgunAFlyboy 10 місяців тому

    I saw a layoff come and go at a big co I worked for that the GM (brand new to the org with no clue who did what) based who got cut 100% on the content of voluntary feedback forms you had to find and choose to fill out. I was sending these out regularly to attempt to make a case for my getting promoted, but a guy that had been on our team 15+ years and was vital to its operation got canned because he was focused on work and wasn't sending out peer review forms. That manager was kind of a disaster and just wanted to outsource stuff to india, so I'm glad she didn't last.

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Sounds like a mess glad you're on your feet thanks for the story from the trenches

  • @mightywurlitzer
    @mightywurlitzer 10 місяців тому

    "Elite and top professionals don't get fired"... that's a bit like saying good people NEVER get cheated on by their spouses. You'd expect a CTO to be a bit more clever than to see the world in non-negotiable absolutes.

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Yeah it was honestly strange and if I knew them I might ask what life experience gave them the urge to jump to such a confident conclusion about a stranger in another country in defense of an as yet unnamed company. Execs may need to make snap decisions sometimes but you don't need to go out of your way to do it on your time off! Could've asked a question. I try to resist getting confrontational but that sort of thing seems important to push back on, because who knows when the next time some hiring manager like them is going to discount a candidate for getting laid off?

  • @steveasher
    @steveasher 10 місяців тому

    As you allude to in your overlay of the Federal Funds Rate and tech layoffs, we are learning just how exposed we are to cyclical risk. I probably have one more sizable economic downturn to survive before retirement, and I'm already giving considerable thought to my strategy for being better positioned for the next one.

  • @arefin-huq
    @arefin-huq 10 місяців тому

    I see that Dafny has support for bounded integer types. I wonder if ensuring the invariant "0 <= quality <= 50" would be easier with a bounded type. (Of course the fact that Sulfuras has quality = 80 makes it more complicated.)

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Thanks for watching, Fin! Yes, I'm still new to this but it seems like at least it would have been more idiomatic Dafny to use "nat" or maybe a more specialized: type Quality = n: nat | n <= 80 The built in natural number type itself is really just: type nat = n: int | 0 <= n But as you point out it doesn't handle both bounds, you'd still need the pre/post conditions to check it based on the name. If I wanted to model it directly in Dafny's type constructs I think there are both OOP and FP ways: inheritance (so one Item subclass always returns 80) or even Algebraic Data Types type Quality = n: nat | n <= 50 datatype Item = Sulfuras | Item(name: string, sellIn: int, quality: Quality) Maybe a weird use of ADTs but now no behavior about Sulfuras needs to be asserted because it has no properties to change. Good luck refactoring our way there though :)

  • @NitsanAvni
    @NitsanAvni 10 місяців тому

    Some thoughts. Mutation testing: How would the equivalent of mutation testing look like for these proofs? Let's say you want to make sure your proof represent the current implementation in full. A mutator might mutate the code in a sandbox and validate that mutants are killed by the proofs. Refactoring: Even while relying on these proofs while refactoring, I feel we should go for something like lift up conditional and other small safe steps, instead of building up a new implementation from scratch. Thank you for these! I'm learning a lot :)

    • @craftvscruft8060
      @craftvscruft8060 10 місяців тому

      Great ideas, Nitsan. Yes, in similar ways that we can discover gaps in tests we can find gaps in specs ("underspecification"), those include review and mutation testing. Formal verification doesn't remove the need for any trust, just moves it to very well-defined areas - any problems must be either in the spec or the prover itself. Often that's a good tradeoff, I see it as a judgement call similar to filling out a test pyramid. Small steps are great as always. In a way I did develop the replacement incrementally because I specified it as equivalent for one item type at a time, but a better way to show that could have been to make the original implementation delegate to the new one for each case as I went. Since you've done TDD training you'd likely have more thoughts about the best ways to present these concepts, look forward to talking more.

  • @NitsanAvni
    @NitsanAvni 10 місяців тому

    Beautiful stuff!

  • @NitsanAvni
    @NitsanAvni 11 місяців тому

    Beautiful and inspiring!! 👏

    • @craftvscruft8060
      @craftvscruft8060 11 місяців тому

      Thanks, Nitsan! You should come on the channel sometime, maybe think about a topic you'd like

  • @craftvscruft8060
    @craftvscruft8060 11 місяців тому

    Despite some mistakes, I didn't reshoot the demo because this time the point is to embrace the disorientation of being at an early stage of practice. If you're trying follow along learning Cursorless, here's some Errata: It didn't capture "each" for "e" when I voice-typed the alphabet. A few times I used "find" instead of "fine" as the "F" phoneme, though the recognizer corrected it. When I said "delete char left fourth", I accidentally combined several ways to do it: Talon's "clear char left forth", "delete fourth" or Cursorless "chuck last four chars" would have been correct. When I "chuck line" and immediately recreated an empty line with "pour line", that's better as a single command "clear line".

  • @RodrigoCubillosCl
    @RodrigoCubillosCl 11 місяців тому

    I totally agree with you Kyle, about the things that is beneficial about AI (detecting the intent) and about creating an environment where the individual collaboration can be priced

  • @GilesBathgate
    @GilesBathgate 11 місяців тому

    Well one solution would be to be autotelic. Everyting you do is also an investment in your own understanding, which can never be thrown away by some upper management.

  • @mrd6869
    @mrd6869 Рік тому

    One more thing. Never ever under estimate nerds with no girlfriends and lots of money🤣 They're dangerous

  • @mrd6869
    @mrd6869 Рік тому

    Its early. Lets have this convo after GPT5 and Google Gemini drop. We'll see what they will and wont be. I dont think they will be this AGI idea either but i do think they be a part of a larger puzzle. And even if they arent,they STILL are gonna be powerful. I have a few applications that are waiting for them to drop

    • @craftvscruft8060
      @craftvscruft8060 Рік тому

      Thanks for the thoughts! Agreed it's an important puzzle piece we didn't have before - whatever the puzzle ends up looking like. I'm extrapolating best I can on what the limits of LLMs and to a lessor extent Deep Learning in general, but I've been surprised before and will be again. I also think it's possible to target AGI as an asymptote without losing focus on managing the present impact of "lessor" systems along the way. A troubling pattern I see is ignoring current needs to fixate on very hypothetical futures, not all AGI proponents do that so I should't paint them all with the same brush.

  • @SFM191
    @SFM191 Рік тому

    This is how marvel villains are born

  • @stevend1070
    @stevend1070 Рік тому

    Wow, I didn't know Chat GPT was a crafter. That was some great advice.