{"action":"created","issue":{"url":"https://api.github.com/repos/dart-lang/site-www/issues/214","repository_url":"https://api.github.com/repos/dart-lang/site-www","labels_url":"https://api.github.com/repos/dart-lang/site-www/issues/214/labels{/name}","comments_url":"https://api.github.com/repos/dart-lang/site-www/issues/214/comments","events_url":"https://api.github.com/repos/dart-lang/site-www/issues/214/events","html_url":"https://github.com/dart-lang/site-www/pull/214","id":200256429,"number":214,"title":"Define soundness more correctly","user":{"login":"thejameskyle","id":952783,"avatar_url":"https://avatars.githubusercontent.com/u/952783?v=3","gravatar_id":"","url":"https://api.github.com/users/thejameskyle","html_url":"https://github.com/thejameskyle","followers_url":"https://api.github.com/users/thejameskyle/followers","following_url":"https://api.github.com/users/thejameskyle/following{/other_user}","gists_url":"https://api.github.com/users/thejameskyle/gists{/gist_id}","starred_url":"https://api.github.com/users/thejameskyle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/thejameskyle/subscriptions","organizations_url":"https://api.github.com/users/thejameskyle/orgs","repos_url":"https://api.github.com/users/thejameskyle/repos","events_url":"https://api.github.com/users/thejameskyle/events{/privacy}","received_events_url":"https://api.github.com/users/thejameskyle/received_events","type":"User","site_admin":false},"labels":[{"id":421018044,"url":"https://api.github.com/repos/dart-lang/site-www/labels/cla:%20yes","name":"cla: yes","color":"0052cc","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2017-01-12T01:36:52Z","updated_at":"2017-01-12T17:37:02Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/dart-lang/site-www/pulls/214","html_url":"https://github.com/dart-lang/site-www/pull/214","diff_url":"https://github.com/dart-lang/site-www/pull/214.diff","patch_url":"https://github.com/dart-lang/site-www/pull/214.patch"},"body":"Hi!\r\n\r\nSo quick nit-picky suggestion. I don't want to come off as pedantic or anything like that. I just want to make this suggestion to make sure that people are learning the correct definition of soundness.\r\n\r\nImplicit nullability is not really a \"sound\" behavior of a language. Unless of course the language accounts for that nullability everywhere. I don't know where Dart falls on this, but I do think this small blurb leaves people with the wrong impression.\r\n\r\nI think it might also be useful to give a more complete definition of soundness, maybe even contrasting it with completeness.\r\n\r\nI'm working on a new documentation for [Flow](https://flowtype.org/) right now and here's what I wrote about this topic:\r\n\r\n> In type systems, ***soundness*** is the ability for a type checker to catch every single error that *might* happen at runtime. This comes at the cost of sometimes catching errors that will not actually happen at runtime.\r\n> \r\n> On the flip-side, ***completeness*** is the ability for a type checker to only ever catch errors that *would* happen at runtime. This comes at the cost of sometimes missing errors that will happen at runtime.\r\n> \r\n> In an ideal world, every type checker would be both sound *and* complete so that it catches *every* error that *will *happen at runtime.\r\n\r\nIf this is useful to you, feel free to use any or all of that.\r\n\r\nThanks 😸 "},"comment":{"url":"https://api.github.com/repos/dart-lang/site-www/issues/comments/272229370","html_url":"https://github.com/dart-lang/site-www/pull/214#issuecomment-272229370","issue_url":"https://api.github.com/repos/dart-lang/site-www/issues/214","id":272229370,"user":{"login":"thejameskyle","id":952783,"avatar_url":"https://avatars.githubusercontent.com/u/952783?v=3","gravatar_id":"","url":"https://api.github.com/users/thejameskyle","html_url":"https://github.com/thejameskyle","followers_url":"https://api.github.com/users/thejameskyle/followers","following_url":"https://api.github.com/users/thejameskyle/following{/other_user}","gists_url":"https://api.github.com/users/thejameskyle/gists{/gist_id}","starred_url":"https://api.github.com/users/thejameskyle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/thejameskyle/subscriptions","organizations_url":"https://api.github.com/users/thejameskyle/orgs","repos_url":"https://api.github.com/users/thejameskyle/repos","events_url":"https://api.github.com/users/thejameskyle/events{/privacy}","received_events_url":"https://api.github.com/users/thejameskyle/received_events","type":"User","site_admin":false},"created_at":"2017-01-12T17:37:02Z","updated_at":"2017-01-12T17:37:02Z","body":"Yup, I already agreed that implicit nullability is fine as long as the language accounts for it:\r\n\r\n> Implicit nullability is not really a \"sound\" behavior of a language. Unless of course the language accounts for that nullability everywhere.\r\n\r\nBut I just want to raise the issue that you are defining \"soundness\" for the first time for readers here, I think it's important that you leave them with a more generalized description.\r\n\r\nOf course soundness and completeness are not a definitive thing for verifying a program's validity, but they have well defined goals.\r\n\r\nI think this small bit about nullability only serves to confuse the readers initial understanding of soundness. It would be more useful to break this section apart into:\r\n\r\n1. Explain soundness in a general sense\r\n2. Explain what soundness means in Dart\r\n\r\nI think this would improve understanding of both soundness and Dart."}}
{"actor":{"display_login":"thejameskyle"}}