Feda /dev/ - No Javascript allowed

#4398 que el tipado estatico no reduce bugs? Cuelgo la llamada.

#4419 El hello world de la verificacion, funcion division.

fun division (dividendo: Int, divisor:Int): Int = dividendo / divsor

Que pasa si divides por 0? Cambias el Tipado para que devuelva un Maybe o creas un tipo NonZeroInt "lo unico que haces" es mover a un lado o a otro el if... y añadir verborrea "logica". Sigue siendo responsabilidad del pica codigo. Sin entrar en casos complejos en runtime. Hay lenguajes que hacen una cosa u otra para solucionar esto pero no resuelven el problema. Por tanto tambien interpreto lo mismo que ha dicho, no resuelve bug porque la posibilidad sigue ahi aparte verborrea.

Si pienso en como utilizo los verificadores y pienso en los lenguajes que lo hacen en compilacion sigo teniendo problemas en entender como te pueden resolver algunos bugs en runtime, entiendo que no solo es verificar en compilacion (esto es lo que yo hago y es una jodienda) sino que al llamar las funciones en runtime tienen el codigo para verificar... No se si esto es lo que significaria evitar bugs porque tendria sus limitaciones.

Recomiendo los primeros capis de: https://ucsd-progsys.github.io/liquidhaskell-tutorial/01-intro.html
Y verificaicon en general sobretodo busca cosas de Z3 que hay muchisimo material y es facil de entender.

Creo que esto en 10 años no se usara en nigun lado, ni 20. Menciono al vegano que en otro hilo dijo que picaba en estos lenguajes @Wei-Yu

Yo de las movidas de verificación y demás paso bastante la verdad xd

Con rust cacharreo un poco cuando me da por ahí y suelo leer lo qeu la gente va hablando o las discusiones abiertas de diseño porque está guay, pero al margen de eso lo poquísimo que hago en mi tiempo libre de picar teclas es 99% C# o typescript, por pura comodidad de tooling.

Este mes empecé a escribir un cliente para soulseek en typescript, intentando adaptar otro en js que me parece una chusta pero está funcional, y también estuve dándole patadas a las Expressions de .net para ver qué cosas se pueden hacer con ellas, quería ver cómo de flexible es el generalizar la construcción de predicados type safe (aunque no sé si al usar reflection para pillar las propiedades se puede decir que algo es typesafe? xd) para dinamizar queries, rollo tirarle un modelo indicando parámetros de búsqueda y que te haga la query entera solo.

#4421 que cojones tendra que strong typing con verificacion formal, ya estas oyendo campanas sin saber donde como siempre.

#4423 reflection no es type safe, si te quieres atener a eso siempre tendras que hacer algo que genere parte del query basado en el tipo estatico.

#4426 me vas a venir a hablar de verificacion formal cuando tuve 2 asignaturas en la carrera.

Y sabes para que me valieron? Para aprender que la programacion desde el mundo de yupi de la logica formal es un circlejerk de gente que no ha programado en su vida, en el mundo real no sacas business logic adelante parandote a pensar si esta verificada o no.

#4434 Yo una vez hice un tests de esos (no de amazon, de otra empresa de software)... pero era en plan ¿te sientes un lider? ¿si un compañero la pifia que harías? y etc...

#4438 XD por aquí igual. Llevo desde el jueves a hoy habré hecho como 25 horas, haciendo nuevas subredes para la VPN, configurando equipos, metiendo IP's en whitelist, ...

hay que echarle una mano a los pelacables