I overslept and ended up an hour and a half late for a two-hour exam once. It was a ridiculous exam too; one question, "here's the specification for a weirdo CPU's instruction set, these are your input and output pins, draw me a logic diagram for a CPU that implements it using only NAND by hand on 8.5 by 11 paper." Figuring out how to implement it wasn't that hard, figuring out how to draw a diagram that was legible in too small a space would have been hard no matter how much time there was. I got an A, I think more for being one of three people who didn't drop the class than because he actually managed to interpret the Jackson Pollock diagram I gave him.I still have nightmares about sleeping through undergrad exams
Man, I could use some more success stories on this subject. Nice. That sounds like an adrenaline-fueled scribblefest. Cheers to that A!
shit, I hate these kinds of exams. I had an exam last year (which I passed, phew) where I had to write formal proofs for a computer program. So I had to frantically scrawl logical statements between every line. That really hurt my hand but it still beats diagrams.
I assume you're talking about Hoare logic, and yes, they still teach it in the more theoretical-CS-inclined departments and it's often at least given a mention in other programmes. In summary, Hoare logic gives you a way to prove the correctness of computer programs by writing what you know to be true at each stage of the execution of the program as a series of formal mathematical statements. Imagine you're some code to square a number, on the first line you might write something like "the variable x equals the number v, where v is the value that was passed to this program" and on the last line you might write "the variable x equals the number v * v". The goal of writing the proof is essentially to show logically how you get from one to the other by transforming that first statement into the last one. Separation logic basically extends this framework by adding a collection of extra rules that allow you to 1. deal with concurrent programs that operate on a shared bit of information and 2. handle programs that use pointer-based data structures. This transforms Hoare logic from being a sorta clunky tool for theoreticians to something that can be used to verify programs in the Real World™ or at the very least detect bugs that aren't covered by syntactic (grammar) or simpler forms of semantic analysis (such as type systems - e.g. "do not let the user multiply the word 'hello' by 3"). In business scenarios, you wouldn't actually write these statements out by hand, but they would be used automatically by various software tools (basically bug-finders). One of its inventors, Peter O'Hearn got head-hunted by Facebook, who now use it to statically detect bugs in their code. Also woah woah I just noticed they have developed an open-source application that uses it!!
Oh, I remember, I just never saw it again after I graduated. I figured it was one of those things like designing analog computers that were fun but sure to be on their way out when the generation of professors who remembered building the things retired.
Yeah I don't expect to see it again... There are certainly a few subjects that, when asked about the non-academic applications, the lecturers tend to shuffle their feet awkwardly or deliver some obviously-rehearsed spiel. I guess academia is a place for those ideas to stay alive, in the hope that some future discovery then brings them back to life in an altered form. It's happened before, right? There were quite a few people in my department who seemed to be emotionally invested in the return of symbolic AI. We can only wait.
I actually have a few expert systems in production, but you'd have to have to be really into GOFAI to recognize them as such. I pointedly didn't tell my bosses I was solving those problems with AI, because if you tell people you're doing AI they assume you're doing something overly ambitious and say 'no'. I bet there are a lot of those out there.
Yeah! Open source is great and all, but so much code exists inside organisations and there's no telling what kinds of methods they're using. I have a friend at Google who mentioned offhand that employees can sift through billions of lines of internal code. I wonder how much internal software itch-scratching has found totally novel methods of solving problems. I'm not sure if it's really possible to know.