Podcast appearances and mentions of alonzo church

Fredrik talks to Pedro Abreu about the magical world of type theory. What is it, and why is it useful to know about and be inspired by? Pedro gives us some background on type theory, and then we talk about how type theory can provide new ways of reasoning about programs, and tools beyond tests to verify program correctness. This doesn’t mean that all languages should strive for the nirvana of dependent types, but knowing the tools are out there can come in handy even if the code you write is loosely typed. We wrap up with some further podcast tips, of course including Pedro’s own podcast Type theory forall. Thank you Cloudnet for sponsoring our VPS! Comments, questions or tips? We a re @kodsnack, @tobiashieta, @oferlund and @bjoreman on Twitter, have a page on Facebook and can be emailed at info@kodsnack.se if you want to write longer. We read everything we receive. If you enjoy Kodsnack we would love a review in iTunes! You can also support the podcast by buying us a coffee (or two!) through Ko-fi. Links Pedro Type theory Type theory forall - Pedro’s podcast Chalmers The meetup group through which Pedro and Fredrik met Purdue university Bertrand Russell The problem of self reference Types Set theory Kurt Gödel Halting problem Alan Turing Turing machine Alonzo Church Lambda calculus Rust Dependent types Formal methods Liquid types - Haskell extension SAT solver Property-based testing Quickcheck Curry-Howard isomorphism Support Kodsnack on Ko-fi! Functional programming Imperative programming Object-oriented programming Monads Monad transformers Lenses Interactive theorem provers Isabelle HOL Dafny Saul Crucible Symbolic execution CVC3, CVC5 solvers Pure functions C# Algebraic data types Pattern matching Scala Recursion Type theory forall episode 17: the first fantastic one with Conal Elliot. The discussion continues in episode 21 Denotational types Coq IRC Software foundations - about Coq and a lot more The church of logic podcast The Iowa type theory commute podcast Titles Type theory podcasts Very odd for some people Brazilian weather Relearning to appreciate The dawn of computer science Layers of sets Where types first come in Bundle values together The research about programming languages If you squint your eyes enough Nirvana of type systems Proofs all the way down Extra guarantees If your domain is infinite Formal guarantees The properties of my system What is the meaning of my program? Building better systems

What is a program? Your answer to this question will determine the paradigm through which you view programming. During this episode, you'll come to understand how things change once you develop an awareness of your paradigm, and what. To kick off this episode, Stephanie shares key insights she took from Planet Argon's 2024 Ruby on Rails survey and dives deeper into her history with Ruby on Rails. Next, we dive into the definition of a paradigm and unpack three different paradigms you might hold as a developer: procedural, object-oriented, and functional. Considering how each of these impacts the way that you might approach your work as a developer, and what you can learn from the ones that are less familiar to you. Joël describes his scripting style and evaluates the concept of pure functions and their place in development, and we close by digging deeper into how your paradigm might impact the code that you write. Tune in to hear all this and more. Key Points From This Episode: The EPI feature that Joël has started to build out for his client. Why Stephanie is excited about the results of Planet Argon's 2024 Ruby on Rails community survey. What a procedural program is: programming envisions a program as a series of instructions to a computer. Defining an object-oriented paradigm: programming envisions a program as the behavior that emerges from objects talking to each other. How a functional paradigm envisions a program as a series of data transformations. Alan Turing and Alonzo Church's approach to understanding this. How a lot of the foundations of computer science came to be built before we had computers. Using Ruby to make judgments and assessing whether or not this is a procedural habit. Why Joël describes his scripting style as being very procedural. Unpacking the meaning of functional programming. Evaluating the concept of pure functions. Considering how your paradigm may impact the Ruby code that you write. Links Mentioned in Today's Episode: 2024 Ruby on Rails Community Survey (https://railsdeveloper.com/survey/2024/) Church-Turing Thesis (https://ocw.mit.edu/courses/24-242-logic-ii-spring-2004/489f7e42fb619645158d7c21a8fb83ad_chuh_trng_thesis.pdf) Dynamic type systems are not inherently more open (https://lexi-lambda.github.io/blog/2020/01/19/no-dynamic-type-systems-are-not-inherently-more-open/) What is Functional Programming? (blog.jenkster.com/2015/12/what-is-functional-programming.html) Blocks as an abstraction vs for loops (https://thoughtbot.com/blog/special-cases) Functional core imperative shell (https://www.destroyallsoftware.com/screencasts/catalog/functional-core-imperative-shell) Testing objects with a functional mindset
 (https://thoughtbot.com/blog/functional-viewpoints-on-testing-objectoriented-code) The Bike Shed (https://bikeshed.thoughtbot.com/) Joël Quenneville on LinkedIn (https://www.linkedin.com/in/joel-quenneville-96b18b58/) Support The Bike Shed (https://github.com/sponsors/thoughtbot)

The subject of this episode's paper — Propositions as Types by Philip Wadler — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once: General recursive functions by Gödel in 1934, with functions of sets of natural numbers. Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions. Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape. Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program. The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation? Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more. And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable Strange Loop talk), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation. Links => patreon.com/futureofcoding — but only if you back the Visual Programming tier!! I'm warning you! Wadler's Strange Loop talk Propositions as Types Cocoon is good. It's not, like, Inside or Limbo good, but it's good. Actually, just play Inside. Do that ASAP. Hollow Knight, also extremely good. Can't wait for Silksong. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great. Chris Martens has done some cool work (eg) bringing together linear logic and games. Meh: Gödel, Escher, Bach by Douglas Hofstadter Yeh: Infinity and the Mind by Rudy Rucker Heh: To Mock a MockingBird by Raymond Smullyan. The hierarchy of automata Games: Agency as Art The Incredible Proof Machine is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you. "Stop Doing Logic" is part of the Stop Doing Math meme. Unrelated: Ivan's song Don't Do Math. Bidirectional Type Checking, a talk by David Christiansen List Out of Lambda, a blog post by Steve Losh Nobody noticed that these links were silly last time, so this time I'm drawing more attention to it: Ivan: Mastodon • Email Jimmy: Mastodon • Twitter This link is legit: DM us in the FoC Slack https://futureofcoding.org/episodes/068See omnystudio.com/listener for privacy information.

On this ID the Future, host Wesley J. Smith talks with polymath and Human Nature author David Berlinski about the philosophy of mathematics, the corruption of science, the burning of Notre Dame, modern Europe's curious incapacity to build graceful, beautiful structures, and what's driving the devolution of Western society. But before any of that, Berlinski relates the dramatic story of how his parents, European Jews, escaped the Nazis only by the skin of their teeth. This is Part 1 of a two-part conversation borrowed with permission from Wesley J. Smith's Humanize podcast. Source

What makes mankind special? And what does it mean to flourish on the frontier of a technological future? Robert J. Marks discusses new technology, what artificial intelligence can and can’t do, and the ethical implications of artificial intelligence with Gretchen Huizinga. This interview was originally published by the Beatrice Institute and is repeated here with their permission. Show Notes 01:32… Source

The Diem blockchain, which was initiated in 2018 by Facebook, includes a novel programming language called Move for implementingsmart contracts. The correctness of Move programs is especially important because the blockchain will host large amounts of assets, those assets are managed by smart contracts, and because there is a history of large losses on other blockchains because of bugs in smart contracts. The Move language is designed to be as safe as we can make it, and it is accompanied by a formal specification and automatic verification tool, called the Move Prover. A project to specify and formally verify as many important properties of the Move standard library is now well underway. This talk will be about the goals of the project and the most interesting insights we've had as of the time of the presentation. The entire blockchain implementation, including the Move language, virtual machine, the Move Prover, and near-final various Move modules are available on http://github.com/libra About the speaker: David L. Dill is a Lead Researcher at Facebook, working on the Libra blockchain project. He is also Donald E. Knuth Professor, Emeritus, in the School of Engineering at Stanford University. He was on the faculty in the Department of Computer Science at Stanford from 1987 until going emeritus in 2017. Prof. Dill's research interests include formal verification of software, hardware, and protocols, with a focus on automated techniques, as well as voting technology and computational biology. For his research contributions, he has received a CAV award and Alonzo Church award. He is an IEEE Fellow, an ACM Fellow and a member of the National Academy of Engineering and the American Academy of Arts and Sciences. He also received an EFF Pioneer Award for his work in voting technology and is the founder of VerifiedVoting.org, an organization that champions trustworthy elections.

Tercera entrega de la serie especial dedicada a la programación funcional presentada por Andros Fenollosa. En este tercer episodio le toca el turno a Haskell de la mano de Héctor Navarro, profesor e investigador en el área de Algoritmos y Lenguajes de Programación. Héctor Navarro actualmente trabaja como Ingeniero de Software en Amazon.com. Desde el año 2000 hasta 2018 ha desempeñado su labor de investigador y profesor en la Universidad Central de Venezuela. A pesar de usar primordialmente Java en trabajo diario, sigue siendo un gran entusiasta de Haskell y de la programación funcional. Haskell es un lenguaje de programación funcionalmente puro, con tipado estático y evaluación perezosa. Su nombre fue otorgado por Haskell Curry, matemático y lógico estadounidense que aportó el cálculo Lambda (un sistema para definir funciones y recursión creado por el matemático y lógico Alonzo Church), siendo este muy influyente dentro del lenguaje. Con Héctor Navarro tenemos oportunidad de tratar interesantes cuestiones del lenguaje: ¿Qué pasó por tu cabeza para meterte en la programación funcional?Dime algunas características que te rompieron la cabeza y te enamoraron.¿Qué es Haskell y cuál es su orgien?¿Qué lo hace especial respecto a otros lenguajes?¿Quién usa Haskell y para quién está orientado?¿Qué son las monadas?¿Cuáles son tus frameworks favoritos?Hablemos sobre el Front-End. ¿Existe implementación? ¿Tal vez Elm?¿Cuál crees que es el futuro del ecosistema?¿Existe una comunidad?Recursos y consejos para grumetes. En esta interesante conversación Héctor Navarro nos cuenta detalles relevantes sobre Haskell, aplicaciones, usos, herramientas y recursos. No olvidéis escuchar y visitar los enlaces de los dos primeros episodios de la serie sobre programación funcional: Descubriendo la programación funcional – Elixir con Erick Navarro Descubriendo la programación funcional – Clojure con Vachi

Tercera entrega de la serie especial dedicada a la programación funcional presentada por Andros Fenollosa. En este tercer episodio le toca el turno a Haskell de la mano de Héctor Navarro, profesor e investigador en el área de Algoritmos y Lenguajes de Programación. Héctor Navarro actualmente trabaja como Ingeniero de Software en Amazon.com. Desde el año 2000 hasta 2018 ha desempeñado su labor de investigador y profesor en la Universidad Central de Venezuela. A pesar de usar primordialmente Java en trabajo diario, sigue siendo un gran entusiasta de Haskell y de la programación funcional. Haskell es un lenguaje de programación funcionalmente puro, con tipado estático y evaluación perezosa. Su nombre fue otorgado por Haskell Curry, matemático y lógico estadounidense que aportó el cálculo Lambda (un sistema para definir funciones y recursión creado por el matemático y lógico Alonzo Church), siendo este muy influyente dentro del lenguaje. Con Héctor Navarro tenemos oportunidad de tratar interesantes cuestiones del lenguaje. Notas del episodio en nuestro sitio web https://republicaweb.es/podcast/descubriendo-la-programacion-funcional-haskell-con-hector-navarro/

Tercera entrega de la serie especial dedicada a la programación funcional presentada por Andros Fenollosa. En este tercer episodio le toca el turno a Haskell de la mano de Héctor Navarro, profesor e investigador en el área de Algoritmos y Lenguajes de Programación. Héctor Navarro actualmente trabaja como Ingeniero de Software en Amazon.com. Desde el año 2000 hasta 2018 ha desempeñado su labor de investigador y profesor en la Universidad Central de Venezuela. A pesar de usar primordialmente Java en trabajo diario, sigue siendo un gran entusiasta de Haskell y de la programación funcional. Haskell es un lenguaje de programación funcionalmente puro, con tipado estático y evaluación perezosa. Su nombre fue otorgado por Haskell Curry, matemático y lógico estadounidense que aportó el cálculo Lambda (un sistema para definir funciones y recursión creado por el matemático y lógico Alonzo Church), siendo este muy influyente dentro del lenguaje. Con Héctor Navarro tenemos oportunidad de tratar interesantes cuestiones del lenguaje. Notas del episodio en nuestro sitio web https://republicaweb.es/podcast/descubriendo-la-programacion-funcional-haskell-con-hector-navarro/

Hoy tratamos sobre el modelo computacional propuesto por Alan Turing, conocido como la máquina de Turing. Sus implicaciones, relevancia y similitudes con el cálculo lambda de Alonzo Church, y como estos trabajos derivaron en la Tesis de Church-Turing.

Welcome to the History of Computing Podcast, where we explore the history of information technology. Because understanding the past prepares us for the innovations of the future! Todays episode is about Alan Turing. Turing was an English mathematician, cryptanalyst, logician, and the reason he's so famous today is probably his work in computer science, being the father of what's often called artificial intelligence. He built the first true working general-purpose computer, although the first Turning-Complete computer would be the Z3 from Konrad Zuse in 1941. Turning was born in 1912. From a young age, he was kinda' weird, but really good at numbers and science. This started before he went to school and made for an interesting upbringing. Back then, science wasn't considered as important as it might be today and he didn't do well in many subjects in school. But in 1931 he went to King's college in Cambridge, where by 1935 he was elected a fellow. While there, he reimagined Kurt Gödel's limits of proof and computation to develop a model of computation now common known as the Turning machine, which uses an abstract machine to put symbols on a strip of tape based on some rules. This was the first example of a CPU, or Central Processing Unit. The model was simple and he would improve upon it throughout his career. Turning went off to Princeton from 1936 to 1938, where he was awarded a PhD in math, after having studied lambda calculus with Alonzo Church, cryptanalysis, and built built three of the four stages of an electro-mechanical binary multiplier, or a circuit built using binary adders that could multiply two binary numbers and tinkered with most everything he could get his hands on. To quote Turing: “We can only see a short distance ahead, but we can see plenty there that needs to be done.” He returned to Cambridge in 1939 and then went to Bletchley Park to do his part in the World War II effort. Here, he made five major cryptanalytical advances throughout the war, providing Ultra Intelligence. While at what was called Hut 8 he pwned the Enigma with the bombe, an electro-mechanical device used by the British cryptologists to help decipher German Enigma-machine-encrypted secret messages. The bombe discovered the daily settings of the Enigma machines used by the germans, including which set of rotors was used, their starting positions and the message key. This work saved over 10 million lives. Many of his cryptographic breakthroughs are used in modern algorithms today. Turing also went to the US during this time to help the Navy with encryption and while in the states, he went to Bell Labs to help develop secure speech devices. After the war, he designed the Automatic Computing Engine, what is now known as a Universal Turing machine.This computer used stored programs. He couldn't tell anyone that he'd already done a lot of this because of the Official Secrets Act and the classified nature of his previous work at Bletchley. The computer he designed had a 25 kilobytes of memory and a 1Megahertz processor and cost around 11,000 pounds at the time. In 1952, Turning was rewarded for all of his efforts by being prosecuted for homosexual acts. He chose chemical castration over prison and died two years later in 1954, of suicide. Alan Turing is one of the great minds of computing. Over 50 years later the British government apologized and he was pardoned by Queen Elizabeth. But one of the great minds of the computer era was lost. He gave us the Turing Pattern, Turning Reduction, Turing test, Turing machine and most importantly 10 million souls were not lost. People who had children and grandchildren. Maybe people like my grandfather, or yours. The Turing Award has been given annually by the Association for Computing Machinery since 1966 for technical or theoretical contributions in computing. He has more prizes, colleges, and building and even institutes named after him as well. And there's a movie, called The Imitation Game. And dozens of books detailing his life have been released since the records of his accomplishments during the war were unsealed. Every now and then a great mind comes along. This one was awkward and disheveled most of the time. But he had as big an impact on the advent of the computer age as any other single human. Next time you're in the elevator at work or talking to your neighbor and they seem a little bit… weird - just think… do they have a similar story. To quote Turing: “Sometimes it is the people no one can imagine anything of who do the things no one can imagine.” Thank you for tuning in to this episode of the History of Computing Podcast. We hope you can find the cryptographic message in the pod. And if not, maybe it's time to build your own bo

Today I talk to Professor Philip Wadler, a very accomplished programming language researcher.  Phil walks us through a principle that has guided his career.  That principle is that typed lambda calculus is not invented but a discovery of a deep truth. It is something connected to the mathematical underpinning of the universe itself. It follows from this that functional programming languages are therefore more correct or more deeply justified and fundamental than other languages.  I am probably stating things in a stronger fashion than Phil is comfortable with, but I like fp, so I can be a little hyperbolic. While explaining this principle, that has guided his career, Phil takes us through the history of computer science.  We start with Turing and Alonzo Church.  Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in. Show notes: talk paper   Web page for this episode CoRecursive On Twitter CoRecursive On Itunes

Provavelmente você já precisou utilizar um celular para se locomover em uma cidade desconhecida. Se não tem carro, pode ser que tenha pedido, via algum aplicativo, um veículo que o levasse a uma reunião do outro lado da cidade enquanto, no caminho, lia as principais notícias do dia e, revezando as janelas no navegador, curtia as fotos de seus amigos na festa do final de semana postadas em uma rede social. Quando voltou, à noite e com fome, utilizou outro aplicativo para pedir o jantar que não teve tempo de preparar, e o saboreou ouvindo uma playlist de indie rock fornecida por um outro app, sugerido por uma amiga em uma mensagem instantânea que há pouco recebera. Apesar de você, talvez, não ter se dado conta, esse processo todo só foi possível por causa de um grande número de algoritmos. Podendo ser, simplificadamente, definidos como um conjunto de regras ou etapas que um computador vai seguir para desempenhar uma determinada função, os algoritmos são, como vimos no dia hipotético acima, indissociáveis de grande parte de nossas atividades cotidianas. Apesar das inegáveis vantagens, seu uso suscita preocupações de igual magnitude. Sobre esse tema, o Oxigênio realizou, dentro do projeto Matemática no Ar, da Semana Nacional de Ciência e Tecnologia 2017, uma entrevista, mediada por Gustavo Almeida, com o Engenheiro da Computação Alan Godoy, do CPqD e o Cientista Social Rafael Evangelista, do Labjor/Unicamp. Os algoritmos estão presentes em “tudo que é computação hoje em dia”, afirma Godoy, explicando que foi nas primeiras décadas do século XX que matemáticos como Alan Turing e Alonzo Church começaram a estabelecer as bases para torná-los o que são atualmente. No século XXI seu uso tem se expandido cada vez mais, e, além das aplicações mais corriqueiras, têm sido usados até mesmo para influenciar cenários políticos, intensificar a vigilância sobre as pessoas e guiar seus hábitos de consumo. “Há menos de exagero e mais de um temor fundamentado sobre usos complicados que os algoritmos podem ter”, adverte Evangelista, para quem os algoritmos correm o risco de caírem sob domínio de grupos a serviço de um modelo econômico injusto e centralizador de poder. A discussão ganha relevância, na visão dos entrevistados, a partir do momento que somos nós, enquanto usuários, que fornecemos as informações para alimentar os algoritmos, a cada clique, “like” na rede social, ou aplicativo acionado. Godoy diz que quando se está numa rede social, por exemplo, ela capta uma quantidade imensa de informações, para fornecer ao usuário uma experiência mais individualizada, em virtude do que você tende a achar mais interessante – o chamado engajamento. “Você recebe sugestões que são personalizadas para o seu gosto”. Evangelista complementa que “todos os usos que fazemos geram rastros, e estes rastros alimentam bancos de dados que não são só utilizados para aquele aplicativo que a gente os está fornecendo”. Essa quantidade enorme de dados, levou à criação do conceito de Big Data (grandes dados, em tradução livre), que serve como “alimento” para os algoritmos, que visam, como diz Godoy, “olhar pro histórico pra tentar prever o futuro” e, assim, lhe oferecer produtos, notícias, canais de entretenimento, para receber seu dinheiro ou, quem sabe?, tentar mudar suas opiniões políticas. Oxigênio na SNCT 2017 Esta entrevista fez parte do projeto “Matemática no Ar”, que integrou a programação da 14ª Semana Nacional de Ciência e Tecnologia (SNCT 2017). Foi uma realização do programa de rádio e podcast Oxigênio por meio do Laboratório de Estudos Avançados em Jornalismo (Labjor) da Unicamp em parceria com a Rádio Unicamp. O projeto ainda contou com a colaboração do PHALA (Grupo de Pesquisa em Educação, Linguagem e Práticas Culturais), da Faculdade de Educação (FE) da Unicamp, além do apoio do Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq), do Ministério da Ciência, Tecnologia, Inovações e Comunicações (MCTIC) e do Governo Federal.

Provavelmente você já precisou utilizar um celular para se locomover em uma cidade desconhecida. Se não tem carro, pode ser que tenha pedido, via algum aplicativo, um veículo que o levasse a uma reunião do outro lado da cidade enquanto, no caminho, lia as principais notícias do dia e, revezando as janelas no navegador, curtia as fotos de seus amigos na festa do final de semana postadas em uma rede social. Quando voltou, à noite e com fome, utilizou outro aplicativo para pedir o jantar que não teve tempo de preparar, e o saboreou ouvindo uma playlist de indie rock fornecida por um outro app, sugerido por uma amiga em uma mensagem instantânea que há pouco recebera. Apesar de você, talvez, não ter se dado conta, esse processo todo só foi possível por causa de um grande número de algoritmos. Podendo ser, simplificadamente, definidos como um conjunto de regras ou etapas que um computador vai seguir para desempenhar uma determinada função, os algoritmos são, como vimos no dia hipotético acima, indissociáveis de grande parte de nossas atividades cotidianas. Apesar das inegáveis vantagens, seu uso suscita preocupações de igual magnitude. Sobre esse tema, o Oxigênio realizou, dentro do projeto Matemática no Ar, da Semana Nacional de Ciência e Tecnologia 2017, uma entrevista, mediada por Gustavo Almeida, com o Engenheiro da Computação Alan Godoy, do CPqD e o Cientista Social Rafael Evangelista, do Labjor/Unicamp. Os algoritmos estão presentes em “tudo que é computação hoje em dia”, afirma Godoy, explicando que foi nas primeiras décadas do século XX que matemáticos como Alan Turing e Alonzo Church começaram a estabelecer as bases para torná-los o que são atualmente. No século XXI seu uso tem se expandido cada vez mais, e, além das aplicações mais corriqueiras, têm sido usados até mesmo para influenciar cenários políticos, intensificar a vigilância sobre as pessoas e guiar seus hábitos de consumo. “Há menos de exagero e mais de um temor fundamentado sobre usos complicados que os algoritmos podem ter”, adverte Evangelista, para quem os algoritmos correm o risco de caírem sob domínio de grupos a serviço de um modelo econômico injusto e centralizador de poder. A discussão ganha relevância, na visão dos entrevistados, a partir do momento que somos nós, enquanto usuários, que fornecemos as informações para alimentar os algoritmos, a cada clique, “like” na rede social, ou aplicativo acionado. Godoy diz que quando se está numa rede social, por exemplo, ela capta uma quantidade imensa de informações, para fornecer ao usuário uma experiência mais individualizada, em virtude do que você tende a achar mais interessante – o chamado engajamento. “Você recebe sugestões que são personalizadas para o seu gosto”. Evangelista complementa que “todos os usos que fazemos geram rastros, e estes rastros alimentam bancos de dados que não são só utilizados para aquele aplicativo que a gente os está fornecendo”. Essa quantidade enorme de dados, levou à criação do conceito de Big Data (grandes dados, em tradução livre), que serve como “alimento” para os algoritmos, que visam, como diz Godoy, “olhar pro histórico pra tentar prever o futuro” e, assim, lhe oferecer produtos, notícias, canais de entretenimento, para receber seu dinheiro ou, quem sabe?, tentar mudar suas opiniões políticas. Oxigênio na SNCT 2017 Esta entrevista fez parte do projeto “Matemática no Ar”, que integrou a programação da 14ª Semana Nacional de Ciência e Tecnologia (SNCT 2017). Foi uma realização do programa de rádio e podcast Oxigênio por meio do Laboratório de Estudos Avançados em Jornalismo (Labjor) da Unicamp em parceria com a Rádio Unicamp. O projeto ainda contou com a colaboração do PHALA (Grupo de Pesquisa em Educação, Linguagem e Práticas Culturais), da Faculdade de Educação (FE) da Unicamp, além do apoio do Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq), do Ministério da Ciência, Tecnologia, Inovações e Comunicações (MCTIC) e do Governo Federal.

Nesse episódio eu comento brevemente a chamada Tese de Church (ou tese de Church-Turing), que conecta a ideia intuitiva de computabilidade (ou algoritmo) com noções formais, dadas, por exemplo, pelo lâmbda-cálculo, de Alonzo Church, e pelas máquinas de Turing, do Alan Turing.

Nesse episódio eu comento brevemente a chamada Tese de Church (ou tese de Church-Turing), que conecta a ideia intuitiva de computabilidade (ou algoritmo) com noções formais, dadas, por exemplo, pelo lâmbda-cálculo, de Alonzo Church, e pelas máquinas de Turing, do Alan Turing.

On discute des suites au programme formaliste d'Hilbert, et principalement de la question de la décidabilité. Retrouvez tout le contenu sur : http://www.principia-informatica.fr/

in a translation of a paper on the Analytical Engine, Ada Lovelace improved upon L. F. Menambrea's work by applying rigor to the calculations that he performed. But then she took things one iteration further. In fact, she took things n iterations further. She wrote the first computer program, using the backtracking feature of the Analytical Engine to perform loops. The Lambda Calculus contains only functions. Evaluating a function is merely rewriting it to replace its parameter with its argument. How then can we represent something like numbers in a language with no primitives? We do it by writing a function that calls another function a certain number of times. The function that calls it once is the number 1. The function that calls it 100 times is the number 100. Alonzo Church demonstrated that these "Church Numerals" could be operated upon by other functions to calculate any computable number. We gain a great deal of confidence in our code if we can reason about the value of variables. What better way to know what a variable contains than to make sure it never changes? Immutability is not just a feature of functional programming languages. It's useful in object-oriented languages like C# and Java as well.

Alonzo Church invented The Lambda Calculus as a simple set of rules that, when applied correctly, could compute anything that you could do with a pencil and paper. But all it is is simple replacement. Learn the basics of lambda expressions so that we can build on this theory of computation. As we celebrate pi day in the States (where we put the month in the wrong place -- 3/14/15), let's see how we go about computing the digits of pi. We'll start out with a simple geometric method, and progress through more modern techniques, until we arive at a truly surprising and remarkable formula. When John von Neumann created Game Theory, he showed how it can sometimes find an optamal strategy. But there's one game for which it fails completely. Find out why The Prisoner's Dilemma is such a tricky problem, and how a fair algorithm was found to be the best possible solution.