F* (lenguaje de programación)

Lenguaje de programación funcional inspirado en ML y orientado a la verificación de programas.

F* (pronunciado F star ) 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 programas, incluidas propiedades de seguridad y corrección funcional. El verificador de tipos F* tiene como objetivo demostrar que los programas cumplen con sus especificaciones utilizando una combinación de resolución de teorías de módulo de satisfacibilidad (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 de la cadena 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* se escribía completamente en un subconjunto común de F* y F# y admitía el arranque tanto en OCaml como en F#. Esto se abandonó 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. "FStarLang/FStar". GitHub . Consultado el 23 de abril de 2024 .
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 . Consultado 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 ejecutable .NET #2512". Github . Consultado el 17 de abril de 2023 .
6. "Considerar la posibilidad de eliminar el requisito de que el código F* debe ser válido F# #1737". Github . Consultado el 17 de abril de 2023 .
7. 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 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 basada en pruebas en F*.

Enlaces externos

• Sitio web oficial
• FStarLang en GitHub
• Tutorial de F*