Video original publicado el 27 de Diciembre de 2017:
Comencé estando muy interesado en la psicología y en como la mente funciona. De lo que realmente se tratan los lenguajes de programación es que tenemos esta idea de lo que queremos que el programa realice ¿Cómo podemos expresar eso de forma más directa? La mente, por su puesto, es una cosa muy embrollada, entonces intentar transformar eso en algo formal es una pregunta muy interesante, y me mantuvo ocupado durante toda mi carrera profesional.
Plutus es el lenguaje de contratos inteligentes (smart contract language) desarrollado por IOHK para la plataforma Cardano. Ha habido muchas discusiones respecto a lenguajes de contratos inteligentes desde la comunidad de programación funcional. Aparecieron Simplicity y Michelson, realmente es genial ver ideas de la comunidad de programación funcional y la comunidad de métodos formales tomar ideas y llevarlas a la práctica. Ahora, ambos son lenguajes de extremadamente bajo nivel (low level language), Plutus es más un lenguaje de alto nivel (high level language), es una versión sobre simplificada de Haskell, que esta viendo un uso cada vez más amplio, incluyendo a la plataforma Cardano en si misma. Es un lenguaje un poquito más elevado, tenemos otro apenas por debajo llamado Plutus Core.
Haskell pertenece a una familia de lenguajes de programación llamada lenguajes de programación funcionales. En la mayoría de los lenguajes de programación ya sea Java C++, etc, la principal preocupación es una palabra de memoria, las cosas se escriben dentro de esa memoria, luego tendrás que rastrear todas las las palabras de memoria y preguntarte ¿que hay ahí dentro en este momento? para poder saber lo que esta pasando. Las matemáticas normales no funcionan de esa forma, sencillamente tienes valores y funciones que actúan sobre esos valores y como resultado entregan otros valores en vez de la noción de almacenaje, cuyo contenido podría cambiar. La programación funcional trabaja sobre esa sencilla idea, tenemos maneras de describir valores y hacer que fluyan de un lado a otro.
No se trata de lograr el mayor nivel de eficiencia de la la arquitectura computacional, las computadoras están bien, son realmente eficientes. Lo mas importante al escribir un lenguaje de programación y especialmente en el criptomercado es preguntarte ¿El programa hace lo que realmente quiero que haga? Los lenguajes funcionales son mucho mejores para estos propósitos, muchas instituciones financieras, bancos, lugares de comercio electrónico se están moviendo al uso de programación funcional, exactamente por esta razón, es mas fácil obtener la respuesta que esperas.
¿Es justo decir que Haskell es como las matemáticas?
Si, incluyendo el hecho de que los desabolladores le tienen miedo, si escribes algo en itálica, osea que se parece a matemáticas, los desarrolladores van a decir "no puedo hacerlo". Estoy realmente sorprendido de esa reacción ya que pueden hacer Java Script, el cual a veces involucra un montón de pequeñas reglas que son bastante ilógicas. Las matemáticas son mucho mas lógicas y fáciles de interaccionar creo yo, a los desarrolladores les esta tomando tiempo darse cuenta de esto, Creen que no lo pueden hacer, pero en realidad es mas fácil inclusive. Algunos desarrolladores son intimidados por Haskell y otros lo adoran y se adentran en el.
Entonces, hay dos áreas relacionadas, por un lado Lenguajes de Programación, yo trabajo en la parte de Programación Funcional, y el área relacionada es Verificación Formal. La idea en Verificación Formal es usar la lógica para escribir la descripción de que exactamente el programa debería hacer. Escribir en un programa funcional es mas trabajoso. Luego querrás probar que el trabajo realizado sea el correcto y utilizarás técnicas estándares de prueba. Ahora tenemos un montón de los llamados asistentes de prueba que te permiten chequear que la prueba sea correcta. La idea de las pruebas fue desarrollada por los griegos antiguos, quienes pensaron ¿Que tarea podría ser fácil de realizar por una computadora? Esa era su idea de la lógica. Perfecto! ahora tenemos computadoras! Ahora podemos chequear las pruebas!
Entonces, todo el amontonamiento de datos de computación, que ahora podemos probar es correcto, es realmente muy caro de realizar, lleva un montón de trabajo. Normalmente, no querrás correr un programa probandolo de esta forma. Pero si tu programa esta manipulando millones de dolares, entonces probablemente valga la pena pagar el costo. Es por eso que creo que hay un renovado interés en los Métodos Formales. Estoy agradecido de trabajar en IOHK y particularmente Charles Hoskinson realmente parece estar liderando el movimiento de interconectar todas estas disciplinas.