Hispanopedia Wiki
Articulo de referencia

F* (lenguaje de programación)

[[French Institute for Research in Computer Science and Automation|Inria]] {{cite web |url=https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/ |title=Micr...

Hispanopedia WikiContenido en espanolLectura gratuita

F* (pronunciado F estrella ) es un lenguaje de programación de alto nivel , multiparadigma , funcional y orientado a objetos, inspirado en los lenguajes ML , Caml y OCaml , y destinado a la verificación de programas . Es un proyecto conjunto de Microsoft Research y el Instituto Francés de Investigación en Ciencias de la Computación y Automatización (Inria). [ 1 ] Su sistema de tipos incluye tipos dependientes , efectos monádicos y tipos de refinamiento . Esto permite expresar especificaciones precisas para los programas, incluyendo la corrección funcional y las propiedades de seguridad. El verificador de tipos de F* tiene como objetivo demostrar que los programas cumplen con sus especificaciones utilizando una combinación de resolución de satisfacibilidad módulo teorías (SMT) y pruebas manuales . Para su ejecución, los programas escritos en F* se pueden traducir a OCaml , F# , C , WebAssembly (a través de la herramienta KaRaMeL) o lenguaje ensamblador (a través del conjunto de herramientas Vale). Las versiones anteriores de F* también se podían traducir a JavaScript .

Se introdujo en 2011 [ 3 ] [ 4 ] y se encuentra en desarrollo activo en GitHub . [ 2 ]

Historia

Versiones

Hasta la versión 2022.03.24, F* estaba escrito completamente en un subconjunto común de F* y F# y admitía el arranque en OCaml y F#. Esto se eliminó a partir de la versión 2022.04.02. [ 5 ] [ 6 ]

Descripción general

Operadores

F* admite operadores aritméticos comunes como +, -, *, y /. Además, F* admite operadores relacionales como <, <=, ==, !=, >, y >=. [ 7 ]

Tipos de datos

Los tipos de datos primitivos comunes en F* son bool, int, float, char, y unit. [ 7 ]

Referencias

  1. ^ "Centro conjunto de investigación de Microsoft Inria " . MSR-INRIA .
  2. 1 2 "FStarLang/FStar" . GitHub . Archivado del original el 26 de abril de 2026. Recuperado el 26 de abril de 2026 .
  3. ↑ Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean (septiembre de 2011). Programación distribuida segura con tipos dependientes del valor . ICFP '11: Actas de la 16.ª Conferencia Internacional ACM SIGPLAN sobre Programación Funcional. Vol. 46. Tokio, Japón: Association for Computing Machinery. págs. 266–278 . doi : 10.1145/2034574.2034811 . Recuperado el 17 de abril de 2023 .  
  4. ↑ "El Proyecto F*" . Microsoft . Consultado el 20 de abril de 2023 .
  5. ↑ "fstar.exe ya no se puede compilar en F# como un ejecutable .NET #2512" . Github . Consultado el 17 de abril de 2023 .
  6. ↑ "Considera eliminar el requisito de que el código F* tenga que ser F# válido #1737" . Github . Consultado el 17 de abril de 2023 .
  7. 1 2 Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (14 de enero de 2024). Programación orientada a pruebas en F* (PDF) .

Fuentes

  • Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Mónadas de Dijkstra gratis" . 44.º Simposio ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación .
  • Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Bosque, Simón; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). "Tipos dependientes y efectos multimonádicos en F*" . 43º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación .
  • Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). Programación orientada a pruebas en F* .
  • Sitio web oficial
  • FStarLang en GitHub
  • Tutorial F*