aaronsnoswell

Downvotes - explain why?

Bing Copilot's transcript from me asking it to ELI5. Take with a massive grain of salt, as it's an LLM etc. etc.

  Me: Can you please explain this webpage like I'm five!
  
  Copilot: Sure! Let’s break it down simply:
  
  The Hoare Cube: Imagine a magic cube that helps us understand how to check if computer programs work correctly or not.
  Commands and States: Think of commands as actions and states as places. When you do an action in one place, you might end up in another place.
  Hoare Triples: These are like rules that say, “If you start in a good place and do an action, you’ll end up in another good place.”
  Flipping Switches: By changing some rules (like flipping switches), you can get different ways to check if programs are correct.
  Three Dimensions:
  Reach: Can you get to a place or must you get to a place?
  Direction: Do you go forward or backward?
  Approximation: Do you guess too much or too little about what happens?
  The Cube: All these different ways of checking can be put together into a cube, showing how they relate to each other.
  It’s like a puzzle that helps computer scientists make sure programs do what they’re supposed to do!
  
  Me: Explain more about the Hoare Triples for me? That bit doesn't make sense
  Copilot: Sure! Let’s break down Hoare Triples in a simple way:
  
  What is a Hoare Triple?
  A Hoare Triple is a way to describe what a computer program does.
  It looks like this: {P} C {Q}.
  Parts of a Hoare Triple:
  P: This is the precondition. It describes what needs to be true before the program (or command) runs.
  C: This is the command. It’s the part of the program that does something.
  Q: This is the postcondition. It describes what should be true after the command runs.
  Example:
  Imagine you have a toy box (P) and you want to put a toy car in it ©. After you put the toy car in the box, the box should have the toy car inside (Q).
  In Hoare Triple terms: {Box is empty} Put toy car in box {Box has toy car}.
  Why is it useful?
  Hoare Triples help us make sure that programs do what we expect them to do.
  They are like rules that tell us if we start with certain conditions and do a specific action, we will end up with the desired result.
  Does that help clarify things?
  
  Me: So where do the hoare triples fit geometrically on this cube representation?
  Copilot: Great question! Let’s break it down:
  
  Hoare Triples: These are represented in the cube by different combinations of three dimensions:
  Reach: Whether the states can reach (may) or must reach (must) a certain condition.
  Direction: Whether the logic is forward (from start to end) or backward (from end to start).
  Approximation: Whether the behavior is over-approximated (includes all possible outcomes) or under-approximated (includes only certain outcomes).
  Cube Representation:
  Each corner (vertex) of the cube represents a different combination of these dimensions.
  For example, partial correctness is represented by the combination of may, forward, and over-approximate.
  Incorrectness logic is represented by may, forward, and under-approximate.
  Visualizing the Cube:
  Imagine a 3D cube where each axis represents one of the dimensions (Reach, Direction, Approximation).
  The corners of the cube show how different combinations of these dimensions form different types of Hoare Triples.
  Equivalences:
  Some corners are equivalent, meaning they represent the same logic but from different perspectives.
  For instance, may+forward+over is equivalent to must+backward+over.
  So, Hoare Triples fit into this cube by occupying different corners based on their specific combination of reach, direction, and approximation. This helps in understanding and comparing different program logics systematically!
  
  Me: So is "partial correctness" an example of a Hoare Triple? What is the 'P', 'C', and 'Q' in this case?
  Copilot: Yes, “partial correctness” is an example of a Hoare Triple. Let’s break it down:
  
  Partial Correctness Hoare Triple:
  {P} C {Q} means that if the precondition P is true before running the command C, and if C terminates, then the postcondition Q will be true after C finishes.
  Components:
  P (Precondition): The condition that must be true before the command starts. For example, if you’re sorting a list, P could be “the list is not empty.”
  C (Command): The action or program being executed. In our example, C would be “sort the list.”
  Q (Postcondition): The condition that must be true after the command finishes, assuming it terminates. For the sorting example, Q would be “the list is sorted.”
  Example:
  {List is not empty} Sort the list {List is sorted}.
  In the context of the Hoare Cube, partial correctness is represented by the combination of may, forward, and over-approximate. This means:
  
  May: The command may reach the postcondition.
  Forward: The logic is applied from the start to the end of the command.
  Over-approximate: The behavior includes all possible outcomes.
  This helps ensure that if the program starts in a good state (precondition) and runs correctly, it will end in a good state (postcondition).
  
  Me: So partial correctness isn't one specific hoare triple then, it's referring to a class of hoare triples that share the 'may, forward, over' properties, right?
  Copilot: Exactly! Partial correctness refers to a class of Hoare Triples that share the properties of may, forward, and over-approximate.
  
  Here’s a quick recap:
  
  May: The command may reach the postcondition.
  Forward: The logic is applied from the start to the end of the command.
  Over-approximate: The behavior includes all possible outcomes.
  So, any Hoare Triple that fits these criteria is considered part of the partial correctness class. It’s not just one specific triple, but rather a group of them that all follow these rules.
  
  Me: And I can travel between vertices of the cube by altering one of the properties I want my hoare triples to have?
  Copilot: Yes, exactly! You can move between the vertices of the Hoare Cube by changing one of the properties (reach, direction, or approximation) of your Hoare Triples. Here’s how it works:
  
  Reach:
  May: The command may reach the postcondition.
  Must: The command must reach the postcondition.
  Direction:
  Forward: The logic is applied from the start to the end of the command.
  Backward: The logic is applied from the end to the start of the command.
  Approximation:
  Over-approximate: Includes all possible outcomes.
  Under-approximate: Includes only certain outcomes.
  By changing one of these properties, you move to a different vertex on the cube. For example:
  
  If you start with partial correctness (may, forward, over-approximate) and change the reach property from may to must, you move to total correctness (must, forward, over-approximate).
  This way, you can explore different types of program logics and understand their relationships by navigating through the cube.
  
  Me: Why isn't there a point on the approximation dimension for 'no approximation'? I thought logic was an exact mathematical science?
  Copilot: That’s a great question! Let’s break it down:
  
  Approximation in Logic:
  In program verification, approximation helps us deal with the complexity of programs.
  Over-approximation includes all possible behaviors, even some that might not actually happen.
  Under-approximation includes only certain behaviors, possibly missing some that could happen.
  Why No ‘Exact’ Point?:
  Exact logic would mean capturing every possible behavior of a program perfectly, which is often impractical due to the complexity and undecidability of many program properties.
  Approximations allow us to reason about programs in a manageable way, even if it’s not perfect.
  Mathematical Logic:
  While logic is exact in mathematics, applying it to real-world programs often requires dealing with uncertainties and complexities.
  Approximations help bridge the gap between theoretical logic and practical program verification.
  So, the approximation dimension in the Hoare Cube reflects the practical need to simplify and manage the complexity of verifying real-world programs.

Answer: No.

Not sure why this article made it to front page, but fwiw, I used to work as a research engineer in a role where using a confocal microscope in clinical trial settings was a regular part of my job. AMA :D

+1 I'm also confused about this post. What does 'steal their tokens' mean in this context?

FFS. I've been fighting uphill this past 5 years to get my colleagues, friends, and family onto Signal. This single decision will tank any hope I have of keeping them there. Literally the only reason I'm able to convince non-privacy advocate types to switch to Signal is because it is a drop-in replacement for their existing SMS application.

This decision is idiotic and will cause a mass migration off the platform. Why not take a better approach and work on a better UX to make it clearer when a message thread is secure or not?

[Australia]: "Hold my beer"

Haven't seen any root-level comments asking, so I'll throw this out there: Are there any good alternatives to YouTube?

I've been making tabletop game to enter into competitions (there are lots running!) and my significant other has been experimenting with making home-made ice-cream and sorbet :)

Brilliant :)

This is an intentional design decision in the language - not having lambda functions / functions as first-class citizens makes the code easier to optimize internally.

This is a very interesting idea and looks like a promising execution - I may try this with one of my repos. I have a question: it seems the only license options are IP-locked. What if a developer wants to issue non-IP locked licenses to paying users? This is a feature I would consider enabling - is that something you will support in the future?

Hi! Thanks for sharing. I would love to know what an 'Exponential+ Trend' is. It's no clear from the landing page and I can't find any links to more information about this. Congrats!

Amazing success story! The game is really fun! You should challenge him to add mobile support via accelerator!

I've read the front page and FAQ section but I'm still not 100% clear what this product is. Is it an active noise cancelling app that listens to your environment around the laptop and cancels noise out (like Bose QC25/35 headphones)? Serious comment - I think you need to explain this better on your site.

Completely agree with the OP. Had the experience of learning TF first, then switching to PyTorch. Cannot recommend enough.

Can someone with more karma modify the title to be less click-bait-ey?

If you're interested in learning Reinforcement Learning, then I can't recommend David Silver's lecture series highly enough. Youtube videos and slides are available for the entire thing. http://www0.cs.ucl.ac.uk/staff/D.Silver/web/Teaching.html

Haha. There should be an entry there for 'Oh shit - I just pushed our private keys to the public github repo'.

Possibly related anecdote; A few years ago I purchased a new sim card for my phone with a large Australian mobile carrier. After popping the new card in, I discovered ~10 real human being contacts on the sim that I had never heard of before (not tech support or business, carrier numbers etc.). They had names and everything. Contacted a few of them and couldn't figure out what the common factor was. I lodged a complaint with the carrier and got a personalized letter and call back from their state manager. No explanation why though. Still baffles me today. Do sim cards get re-used?

A very interesting result with big implications for the future AI arms race :) Congratulations and thanks for sharing!

Boeing Research & Technology | Multiple positions | Brisbane, Australia | ONSITE | Au Citizens Only

Interested in building the future of aerospace? Come join the leading internal VR development team for The Boeing Company, based in Brisbane Australia. Develop software that will be used to train the next generation of Pilots and Astronauts. Currently hiring for multiple positions.

- Computational Geometry Research Engineer: https://www.seek.com.au/job/34722911?type=standard&userquery... - Software Engineer: https://www.seek.com.au/job/34685662?type=standard&userquery... - 3D Artist: https://www.seek.com.au/job/34724717?type=standard&userquery...

Applicants must be Australian citizens to meet defence security requirements. Boeing is an Equal Opportunity Employer.

I can answer some questions via twitter (my handle is my HN username).

+1 for this use case!

Can someone explain where the gif image on slide 69 comes from?

Great article - I really enjoyed it. Who are you? Your blog doesn't have an about page.

Can you expand on what you mean by non-sequential and non-hierarchical?

I thought the title said 'Portal', not 'Postal'. Disapointed :P

The exiting thing for me is at 1:30 in the video. Smooth changes in the latent space lead to smooth changes in the shape (eg. the chair arms gradually recede along their longitudinal axis). This means you have good generalisability (the network is robust to input noise) and composablility (the network can produce novel results through transformations in latent space).

I built a barn-door electric drive astrophotography rig for long exposure star photos.