5 ms·

A Generalized Algebraic Theory of Directed Equality

63 points by matt_d 1y ago

weinzierl 1y ago
"See below for a desciption of the contents of the thesis, at four different levels of assumed background knowledge: 'Basic' (no assumed familiarity with type theory and category theory), 'Intermediate' (some familiarity), 'Advanced' (significant assumed familiarity), and 'Expert'." This is a brilliant idea and very well executed. I almost did not click the link because I would put myself into the 'Intermediate' (some familiarity) bucket and most blog posts are either too basic or too advanced for me. Glad I clicked.
cubefox 1y ago
... and for those who were wondering about the TLD: > In our biggest launch to date, Google Registry is adding eight new extensions to the internet: .dad, .phd, .prof, .esq, .foo, .zip, .mov and .nexus, now publicly available at a base annual price through your registrar of choice. > The .phd, .prof, and .esq TLDs are perfect for professionals who want to show off their credentials and expertise. https://www.registry.google/announcements/introducing-8-new-tlds-for-dads-grads-and-techies/ https://www.registry.google/announcements/introducing-8-new-...
- tristramb 1y ago
  ..or for non-professional who want to mislead people into thinking that they have those credentials and expertise.
  - philipallstar 1y ago
    To be fair, though, if you can get funding for your PhD then you can do this already with an actual PhD.
  - pentaphobe 1y ago
    100% Though it's notable [^1] that only in America does "esquire" imply any credentials or expertise Tonnes of non-special boys in the UK get "esquire" as a suffix (maybe some go on the become attorneys, but unrelated :) [1]: EDIT: on second thought - it's not "notable" at all, perhaps "interesting" was the word I sought..
- theknarf 1y ago
  .zip sounds like a terrible idea for a top-level domain.
  - cubefox 1y ago
    I disagree, this sounds perfectly respectable: http://virus.exe.zip/ http://virus.exe.zip/
    - mcdonje 1y ago
      I clicked
- meindnoch 1y ago
  i'm tired boss
  - cubefox 1y ago
    So you don't want to show off your credentials and expertise??
casey2 1y ago
I feel that massive effort is being misdirected because of some fundamental misunderstandings Programming languages, like all languages, exist for communication between humans. A better programming language for a particular task is one that lowers friction needed to communicate ideas about particular programs. The power of modern languages come from us quickly being able to understand programs. All languages rely on convention and assumption. The vast majority of bugs don't come from under-specification, but rather poor/miscommunication. Under-specification might explain why you wasted an hour reading source code to fix a minor problem, poor communication explains why we haven't yet automated every conceivably meaningful task computers are physically capable of already.
- deleted 1y ago
  [deleted]
- ndriscoll 1y ago
  This work is more focused on proof assistants. i.e. programming languages designed for highly generic algorithms (mathematical proofs). I don't see how miscommunication or bugs are possible in this context. The assumptions and conclusions are all laid out in the types. Barring a bug in the type checker or use of e.g. `sorry`, a proof that compiles shouldn't be able to contain a bug.
  - cubefox 1y ago
    A formal proof can contain a "miscommunication bug" if it proves not the exact thing that it was intended to prove. This is just like an ordinary program that doesn't exactly do what it is supposed to do.
    - ndriscoll 1y ago
      The types say exactly what is proved. There's no real room for confusion. With a written proof you could accidentally make some assumption in the middle (like using some lemma that assumes a thing is finite or compact or whatever when you did not state that assumption), but a computer proof cannot do this. It won't typecheck. Reading mathematical sentences (types, basically) is like step one in maturing from baby to toddler in math.
moi2388 1y ago
“Or maybe s and t represent possible states of some computer system, and Hom(s,t) is the type of processes that, when executed in state s, will result in state t. We definitely want to allow these processes to be irreversible” Why? Irreversibility is what prevents computers from theoretically not requiring energy for their computation. I’d rather truly have reversible computation ;)

63 points by matt_d 1y ago

"See below for a desciption of the contents of the thesis, at four different levels of assumed background knowledge: 'Basic' (no assumed familiarity with type theory and category theory), 'Intermediate' (some familiarity), 'Advanced' (significant assumed familiarity), and 'Expert'." This is a brilliant idea and very well executed. I almost did not click the link because I would put myself into the 'Intermediate' (some familiarity) bucket and most blog posts are either too basic or too advanced for me. Glad I clicked.

cubefox 1y ago

... and for those who were wondering about the TLD: > In our biggest launch to date, Google Registry is adding eight new extensions to the internet: .dad, .phd, .prof, .esq, .foo, .zip, .mov and .nexus, now publicly available at a base annual price through your registrar of choice. > The .phd, .prof, and .esq TLDs are perfect for professionals who want to show off their credentials and expertise. https://www.registry.google/announcements/introducing-8-new-tlds-for-dads-grads-and-techies/ https://www.registry.google/announcements/introducing-8-new-...

tristramb 1y ago
..or for non-professional who want to mislead people into thinking that they have those credentials and expertise.
- philipallstar 1y ago
  To be fair, though, if you can get funding for your PhD then you can do this already with an actual PhD.
- pentaphobe 1y ago
  100% Though it's notable [^1] that only in America does "esquire" imply any credentials or expertise Tonnes of non-special boys in the UK get "esquire" as a suffix (maybe some go on the become attorneys, but unrelated :) [1]: EDIT: on second thought - it's not "notable" at all, perhaps "interesting" was the word I sought..
theknarf 1y ago
.zip sounds like a terrible idea for a top-level domain.
- cubefox 1y ago
  I disagree, this sounds perfectly respectable: http://virus.exe.zip/ http://virus.exe.zip/
  - mcdonje 1y ago
    I clicked
meindnoch 1y ago
i'm tired boss
- cubefox 1y ago
  So you don't want to show off your credentials and expertise??

casey2 1y ago

I feel that massive effort is being misdirected because of some fundamental misunderstandings Programming languages, like all languages, exist for communication between humans. A better programming language for a particular task is one that lowers friction needed to communicate ideas about particular programs. The power of modern languages come from us quickly being able to understand programs. All languages rely on convention and assumption. The vast majority of bugs don't come from under-specification, but rather poor/miscommunication. Under-specification might explain why you wasted an hour reading source code to fix a minor problem, poor communication explains why we haven't yet automated every conceivably meaningful task computers are physically capable of already.

deleted 1y ago
[deleted]
ndriscoll 1y ago
This work is more focused on proof assistants. i.e. programming languages designed for highly generic algorithms (mathematical proofs). I don't see how miscommunication or bugs are possible in this context. The assumptions and conclusions are all laid out in the types. Barring a bug in the type checker or use of e.g. `sorry`, a proof that compiles shouldn't be able to contain a bug.
- cubefox 1y ago
  A formal proof can contain a "miscommunication bug" if it proves not the exact thing that it was intended to prove. This is just like an ordinary program that doesn't exactly do what it is supposed to do.
  - ndriscoll 1y ago
    The types say exactly what is proved. There's no real room for confusion. With a written proof you could accidentally make some assumption in the middle (like using some lemma that assumes a thing is finite or compact or whatever when you did not state that assumption), but a computer proof cannot do this. It won't typecheck. Reading mathematical sentences (types, basically) is like step one in maturing from baby to toddler in math.

moi2388 1y ago

“Or maybe s and t represent possible states of some computer system, and Hom(s,t) is the type of processes that, when executed in state s, will result in state t. We definitely want to allow these processes to be irreversible” Why? Irreversibility is what prevents computers from theoretically not requiring energy for their computation. I’d rather truly have reversible computation ;)