Byron Cook: Inside Terminator

The Discussion

• 

  Interesting stuff, Byron does a good job of making it comprehensible. Now if only the same tools could be used for .NET... (I know, I know, I'm dreaming. Perhaps in a few years time?)
  
  It looks like there will soon be very few excuses for not having reliable device drivers at least though!

• 

  Great video. I remember reading a piece some time ago about militairy software, and proofing correct operation of it. If I remember correctly, they where able to proof the complete application/system, not just the device drivers. Now I wander if maybe there are programming languages for which it is much easier to find proof of correct functioning that it is for c(++)?

• 

  really interesting. it reminded me of computer science at university.
  

• 

  ilmar, you need to keep in mind that provable systems for the military and other safety critical applications (especially subsystems on airplanes) are written in a subset of the ADA language called SPARK. they got rid of possibly dangerous or hard to proof constructs and added annotations for static verifiers (a bit like SAL in the microsoft sdks but more elaborate) which resulted in a language that facilitates proofs.
  you might want to read up a bit on ada and spark: it's a fascinating world for die-hard c++ programmers especially.
  
  cheers,
  martin
  

• 

  Regarding X > 0 && Y > 0: What about passing in positive infinities?

• 

  to the above post. You can't pass an infinite positive in a system which can represent only finite numbers, however the different permutations of the state transitions could be infinite (or at least of a much larger order), so hence the point can you terminate the state transitions passing a finite number.
  
  Anyways, Byron made a typo:
  
  he was trying to prove
  (x>0 && y>0 && x`=x && y`=y-1)
                          ||
  (x>0 && y>0 && y`=y-1 && x`=x)
  
  what should be is the following, because the above two are the same, unless I forgot boolean algebra:
  
  (x>0 && y>0 && x`=x && y`=y-1)
                          ||
  (x>0 && y>0 && x`=x-1 && y`=y)
  
  Great stuff, I miss that in my day-to-day .NET life
  

• 

  
  You mention a great blog article by a Chris Broom in the video, but I'm unable to find it.  Do I have the name right?  Can someone post a link?
  
  Thanks,
  
  Jason

• 

  Sounds like halting problem is no longer a problem?