Las pruebas basadas en propiedades (PBT) son una técnica consolidada para validar software: los usuarios escriben propiedades —especificaciones ejecutables— que un framework evalúa repetidamente con datos aleatorios. Los marcos modernos suelen incrustar esas propiedades en lenguajes específicos de dominio superficiales y acoplan su definición al modo en que se ejecutan. Esto limita la personalización: solo cabe lo que el autor del framework previó, y cualquier cambio relevante obliga a reescribir la herramienta desde cero.
Este artículo propone un lenguaje más profundo para propiedades, basado en una incrustación mixta que los autores denominan sintaxis abstracta con enlace diferido. La idea clave es reificar las propiedades como una estructura de datos, desacoplándolas de los property runners que las ejecutan. Esa separación permite tratar las propiedades como objetos manipulables, sobre los que se pueden construir runners distintos sin modificar el código original.
Para validar la propuesta, los autores implementan el lenguaje en dos entornos muy distintos: Rocq, aprovechando los tipos dependientes para garantizar propiedades a nivel de prueba formal, y Racket, sirviéndose de los tipos dinámicos para experimentar con mayor agilidad. A partir de ahí, muestran la flexibilidad del enfoque mediante la creación rápida de prototipos de property runners variados, y ponen de relieve mejoras de testeo específicas que solo son posibles cuando la infraestructura de pruebas es programable. El trabajo se enmarca en la búsqueda de herramientas de verificación más componibles, y conecta con líneas previas como QuickCheck, AFL++ o el fuzzing dirigido, al tiempo que abre la puerta a runners especializados para dominios concretos sin necesidad de reinventar el framework.