Xah Talk Show 2024-01-11 Ep529 Type Theory, WolframLang Machine Learning

• https://youtube.com/live/qo-6Kckxu7o

• 0:19 keyboard intro
• 4:36 type theory
• 4:55 why we need logic
• 7:22 why C++ can't prove everything
• 13:03 URL and proofs
• 19:41 homotopy tail chasing
• 24:00 origin of type theory
• 25:08 lambda cube
• 29:12 no category theory
• 29:58 logic text books
• 33:11 coq
• 34:09 F-star lang
• 34:31 origin meta-lang ocaml fsharp
• 36:58 proof languages
• 38:37 lambda cube
• 39:30 how type systems differ
• 45:36 unicode logic symbols
• 49:34 proof languages
• 51:06 which to choose
• 58:40 elisp image processing
• 1:04:03 WolframLang 14
• 1:17:00 machine learning in WL
• 1:19:48 machine learning demo in WolframLang

• ml (meta lang)
• sml (standard ml, or nj ml)
• caml (category abstract meta lang)
• ocaml (object category abstract ml)
• fsharp (by Microsoft)
• fstar

• proof assistants
• coq
• lean
• fstar
• Kevin Buzzard
• Condensed mathematics
• Logic
• Type theory
• Lambda cube
• Pure type system

• Emacs: Xah Fly Keys
• Ergonomic Keyboard Reviews
• type theory
• Free Math Textbooks
• Xah Unicode Blog
• Unicode: Logic Symbols ∀ ∃

chars = {"ㄱ", "ㄲ", "ㄳ", "ㄴ", "ㄵ", "ㄶ", "ㄷ", "ㄸ", "ㄹ", "ㄺ", "ㄻ", "ㄼ", "ㄽ", "ㄾ", "ㄿ", "ㅀ", "ㅁ", "ㅂ", "ㅃ", "ㅄ", "ㅅ", "ㅆ", "ㅇ", "ㅈ", "ㅉ", "ㅊ", "ㅋ", "ㅌ", "ㅍ", "ㅎ", "ㅏ", "ㅐ", "ㅑ", "ㅒ", "ㅓ", "ㅔ", "ㅕ", "ㅖ", "ㅗ", "ㅘ", "ㅙ", "ㅚ", "ㅛ", "☺", "☻", "😃", "😄", "😅", "🥲", "😆", "😊", "😎", "😇", "😈", "😏", "🥹", "🤣", "🤩", "🤪", "🥳", "🫠", "😁", "😀", "😂", "🤠", "🤡", "🤑", "🤓", "🥸", "🤖", "✝", "☦", ",", "❌", "❎", "Greek", "Cross", "🞡", "🞢", "🞣", "🞤", "✚", "🞥", "🞦", "🞧", "✙", "⛨", "✛", "✜", "✝", "🕆", "🕇", "✞", "✟", "🞨", "🞩", "🞪", "🞫", "🞬", "🞭", "🞮", "⭙", "☓", "⛝", "☦", "☩", "✠", "♰", "♱", "🕈", "☨", "À", "Á", "Â", "Ã", "Ä", "Å", "Ā", "Ă", "Ǎ", "Ǟ", "Ǡ", "Ǻ", "Ȁ", "Ȃ", "Ȧ", "Ẵ", "Ą", "Ḁ", "Ạ", "Ả", "Ấ", "Ầ", "Ẩ", "Ẫ", "Ậ", "Ắ", "Ằ", "Ẳ", "Ặ", "Ⱥ", "à", "á", "â", "ã", "ä", "å", "ā", "ă", "ą", "ǎ", "ǟ", "ǡ", "ǻ", "ȁ", "ȃ", "ȧ", "ẚ", "ạ", "ả", "ấ", "ầ", "ẩ", "ẫ", "ậ", "ắ", "ằ", "ẳ", "ẵ", "ặ", "ḁ", "ᶏ", "♦", "あ", "い", "う", "え", "お", "k", "か", "き", "く", "け", "こ", "s", "さ", "し", "す", "せ", "そ", "t", "た", "ち", "つ", "て", "と", "n", "な", "に", "ぬ", "ね", "の", "h", "は", "ひ", "ふ", "へ", "ほ", "m", "ま", "み", "む", "め", "も", "y", "や", "♦", "ゆ", "♦", "よ", "r", "ら", "り", "る", "れ", "ろ", "w", "わ", "ゐ", "♦", "ゑ", "を"};
imgs = Map[ Rasterize , chars ];
FeatureSpacePlot[ imgs ]