3 ms·

Love the premise. Read the Principles — good ground to stake out! Nitpick though, with: > “Provably correct. We aim for our code to be provably correct; that

Love the premise. Read the Principles — good ground to stake out! Nitpick though, with: > “Provably correct. We aim for our code to be provably correct; that is, covered by automated testing.” Generally, ‘provably correct’ implies formal proofs e.g. ‘formal reasoning’, rather than test coverage. See: https://coq.inria.fr/ https://coq.inria.fr/ ”Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.”

hn_throwaway_69 5y ago
- jpttsn 5y ago
  Have you excluded non-English speakers from reading your comment above?
  - hn_throwaway_69 5y ago
    Really? Apples and oranges. You can easily copy my comment into Google Translate. An app available on the web, iOS and Android, free of charge. I can't use this chat app (to my knowledge) to communicate with friends using this app without spending a lot of money to buy an iPhone or Mac. It's also impractical for me to provide my comment in every popular language in the world. Its even more so impractical to write every comment in a multilingual way. There are two major phone platforms and it's not an onerous ongoing obligation to provide chat apps for each platform.
- BoorishBears 5y ago
  I just want to point out, as someone who's spent a lot of time in the mobile space and worked behind the scenes on some of the most widely used apps out there... If you see an iOS only app, it's because Android users don't pay. Sometimes you just need money to make things work, especially when one of your core goals is not needed external funding. Not everyone can get a 50 million dollar grant... Also you should definitely elaborate on this because it sounds wrong: > Apple offer APIs which make it easy for app developers to exclude and fragment No idea what that's supposed to mean, and sounds like strange Apple bashing. Closest thing I can think of is maybe iMessage apps? But that's a terrible example since the equivalent functionality on other messaging platforms also needs to be messenger specific, that's just kind of core to how they function?
RenderedCarrot 5y ago
Thank you for this clarification. I have updated the language of that section to not use “provably correct” term.

hn_throwaway_69 5y ago

jpttsn 5y ago
Have you excluded non-English speakers from reading your comment above?
- hn_throwaway_69 5y ago
  Really? Apples and oranges. You can easily copy my comment into Google Translate. An app available on the web, iOS and Android, free of charge. I can't use this chat app (to my knowledge) to communicate with friends using this app without spending a lot of money to buy an iPhone or Mac. It's also impractical for me to provide my comment in every popular language in the world. Its even more so impractical to write every comment in a multilingual way. There are two major phone platforms and it's not an onerous ongoing obligation to provide chat apps for each platform.
BoorishBears 5y ago
I just want to point out, as someone who's spent a lot of time in the mobile space and worked behind the scenes on some of the most widely used apps out there... If you see an iOS only app, it's because Android users don't pay. Sometimes you just need money to make things work, especially when one of your core goals is not needed external funding. Not everyone can get a 50 million dollar grant... Also you should definitely elaborate on this because it sounds wrong: > Apple offer APIs which make it easy for app developers to exclude and fragment No idea what that's supposed to mean, and sounds like strange Apple bashing. Closest thing I can think of is maybe iMessage apps? But that's a terrible example since the equivalent functionality on other messaging platforms also needs to be messenger specific, that's just kind of core to how they function?

RenderedCarrot 5y ago

Thank you for this clarification. I have updated the language of that section to not use “provably correct” term.