Yeah if I saw someone wandering around in a suit at Apple I'd assume it was a hardware vendor who somehow broke free from his handlers and was snooping for secrets.
Those were pretty much the only people you'd see hanging around in suits.
So it could be [efficiently?] decidable if you forced the function specification to adhere to certain rules that ensured a standard, easily-comparable format?
It depends on how restrictive your "certain rules" are. It's quite possible to restrict things so much that functions will be comparable in terms of both structure and functionality. But usually that's way too much restriction.
Consider the example of writing a function that does the collatz sequence computation and another function that just returns one. How would you compare them? It will most likely return Equal but even the greatest mathematicians can't say for sure.
Now consider another example where you restrict the function definition to only include simple arithmetic (no control flows i.e. no conditionals no loops no function calls). A good CAS system can already simplify these functions and you can compare them quite easily (though not trivially).
On the other hand, if the rules are restrictive enough to stop the language from being Turing-complete, you could make it work.
There's an interesting design problem there: how do you make a language that's powerful and expressive enough to be useful but simple and restricted enough to solve problems like this reliably?
> There's an interesting design problem there: how do you make a language that's powerful and expressive enough to be useful but simple and restricted enough to solve problems like this reliably?
See theorem proving systems like Coq which use languages that are total. The majority of loops you write while coding obviously terminate (for item in items...) and Coq lets you prove more complex forms of looping terminate so it's not as restrictive as you'd think.
Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program. I know there is some proof-search-based automation available (ie auto), but I understand it's still pretty limited.
Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain. Designing languages like that would let us verify non-trivial properties fully automatically and can save a lot of work for the user, but we end up needing to design a language for each class of task that we care about.
As I said: it's an interesting design problem.
One recent addition to this is the Lean theorem prover, which tries to be similarly powerful and general as Coq but with more provisions for automation via the Z3 SMT solver. I haven't played with it myself but from what I've heard it's a very promising development in making formal verification more accessible to non-experts.
> Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
Pretty much every theorem proving system out there is expressive enough to state whatever program property you want. You can't escape having to automate proofs though.
> Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program.
Yes, it's the most challenging aspect of programming I've ever tried. It's completely impractical and too expensive for most projects right now outside of domains where mistakes cost even more like aviation, medical devices, operating systems, CPU etc.
> The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain.
I'm not really sure what the sweet spot is to be honest or if there is one when you require full automation. Even non-linear arithmetic is undecidable (basically arithmetic where you're allowed to multiply variables together) so you quickly get into undecidable territories for what seem like basic properties. No clever language design idea is going to let you side-step that proof automation is hard which has been worked on for decades. Even writing program specifications requires a skillset most programmers will have to learn.
When you add restrictions to make equalities like this decidable, it usually means less things are equal to each other if that makes sense so the problem is being pushed elsewhere somewhat.
For example, Coq has decidable equality which is crudely described as "simplify both sides as much as possible and if they're syntactically the same then they're equal". So this could be equal depending on how you define plus:
plus(1, plus(1, x)) = plus(2, x)
but this wouldn't be:
plus(1, plus(1, x)) = plus(x, 2)
Long story but "plus" is usually defined by recursion on the first argument and when you put the "x" as the first argument the type checker cannot simplify "plus(x, 2)" any further so it isn't able to simplify both sides to the same form, therefore they're not equal. So this makes equality decidability but now things you intuitively think of as equal aren't equal.
What do you mean? You can write theorems that show plus is associative and commutative for example but that doesn't make the example I gave "equal" in Coq in the sense you normally mean. As I said, it's not intuitive as we're usually very loose in what we mean by "equal".
> The name of the project is “Tectonic,” spelled and pronounced like a regular word because it is one. Enough with the cutesy obscurantism. In cases where the name might lead to ambiguities, it should be expanded to “Tectonic typesetting.”
> If you’re feeling expansive, you can interpret the name as suggesting a large change in the TeX world. Or you can think of it as suggesting a salubrious offering for weary TeX users. Either way, the root of the word does go back to the ancient Greek τέκτων, ”carpenter,” which Donald Knuth — the creator of TeX and a devout Christian — might appreciate.
I enjoy wearing suits to work. Sadly, at some tech companies it is a bad idea nowadays. I wore a suit to work at Google and Facebook and regularly got called security on. I made sure to always keep my badge close.
Until recently I had a worked with a friend who wears nothing but suits, not just at work but in day to day life. People found it odd for a few months but then he quickly got a rep as that really well dressed guy and most folk enjoyed it. Admittedly it helped that most of his suits were a bit more out there than typical business suits. Think slightly hipster barbershop quartet. The man had some damn nice jackets.
As long as they are decent quality. I have an aquaintance who dresses up for events in cheap terrible suits and he looks like a caracature of a used car salesman. He is genuinely embarrasing to be around, but thinks the attention is positive, because people recodnise him now. Nice guy, but I can't help but think more people need to know, so they don't do the same.
Same, and same. I get questions about which job I'm there to apply for.
I wear suits to work because it is counter-culture, and they make me look like a programmer version of James Bond. People who don't like wearing suits clearly have never worn a tailored suit.
Boy, this seems pretty surprising. Other folks at google or facebook decided that you looked out of place and then called security? What do executives at FB and google wear?
I work at Google and I don't think I've ever seen an employee wear a suit to work, maybe a blazer but definitely no ties. People who are at a certain level of leadership and above seem to wear button down shirts most of the time, usually with jeans.
The only time I saw people in formal attire was at a masquerade-themed holiday party.
